UC5 Eval Criteria SCP-2/Mapping 1-3
Construction of Event-B model to verify the system design against the formalised requirements
https://repo.valu3s.eu/use-cases/demonstrators-evaluation-results-1/demo-6/uc5-eval-criteria-scp-2-mapping-1-3
https://repo.valu3s.eu/@@site-logo/logo_valu3s_green_transparent.png
UC5 Eval Criteria SCP-2/Mapping 1-3
Construction of Event-B model to verify the system design against the formalised requirements
UC5
Modelling of system in Event-B, using a simulink model and natural language requirements as quidance, supporting automated verification tools in detecting safety requirement violations.
- UC5_TC_1 Preconditions: Aircraft is in operating mode M and sensor S value deviates at most +/-R % from nominal value; Input conditions / steps: Observed aircraft thrust is at value V1 and pilot input changes from A1 to A2; Expected results: Observed aircraft thrust changes and settles to value V2, respecting control objectives (settling time, overshoot, steady state error).
- UC5_TC_2 Preconditions: Aircraft is in operating mode M and sensor S value is not available (sensor is out of order); Input conditions / steps: Observed aircraft thrust is at value V1 and pilot input changes from A1 to A2; Expected results: Observed aircraft thrust changes and settles to value V2, respecting control objectives (settling time, overshoot, steady state error.
- UC5_TC_3 Preconditions: Aircraft is in operating mode M and sensor S value deviates at most +/-R % from nominal value; Input conditions / steps: Observed aircraft thrust is at value V1 and perturbations in non-pilot input cause it to change to V2; Expected results: Observed aircraft thrust returns to value V1, respecting control objectives (settling time, overshoot, steady state error).
- UC5_TC_4 Preconditions: Aircraft is in operating mode M and sensor S value is not available (sensor is out of order); Input conditions / steps: Observed aircraft thrust is at value V1 and perturbations in non-pilot input cause it to change to V2; Expected results: Observed aircraft thrust returns to value V1, respecting control objectives (settling time, overshoot, steady state error).
- UC5_TC_5 Preconditions: Aircraft is in operating mode M and sensor S value deviates at most +/-R % from nominal value; Input conditions / steps: Observed aircraft thrust is at value V1 and pilot input changes from A1 to A2; Expected results: Observed aircraft thrust changes and settles to value V2, respecting operating limit objectives (e.g. upper limit in shaft speed).
- UC5_TC_6 Preconditions: Aircraft is in operating mode M and sensor S value is not available (sensor is out of order); Input conditions / steps: Observed aircraft thrust is at value V1 and pilot input changes from A1 to A2; Expected results: Observed aircraft thrust changes and settles to value V2, respecting operating limit objectives (e.g. upper limit in shaft speed).
- UC5_TC_7 Preconditions: Aircraft is in operating mode M and sensorS value deviates at most +/-R % from nominal value; Input conditions / steps: Observed aircraft thrust is at value V1 and perturbations in non-pilot input cause it to change to V2; Expected results: Observed aircraft thrust returns to value V1, respecting operating limit objectives (e.g. upper limit in shaft speed).
- UC5_TC_8 Preconditions: Aircraft is in operating mode M and sensor S value is not available (sensor is out of order); Input conditions / steps: Observed aircraft thrust is at value V1 and perturbations in non-pilot input cause it to change to V2; Expected results: Observed aircraft thrust returns to value V1, respecting operating limit objectives (e.g. upper limit in shaft speed).
- UC5_TC_9 Preconditions: Aircraft is in operating mode M and system parameter P deviates at most +/- R % from nominal value; Input conditions / steps: Observed aircraft thrust is at value V1 and pilot input changes from A1 to A2; Expected results: Observed aircraft thrust changes and settles to value V2, respecting control objectives (settling time, overshoot, steady state error).
- UC5_TC_10 Preconditions: Aircraft is in operating mode M and system parameter P deviates at most +/- R % from nominal value; Input conditions / steps: Observed aircraft thrust is at value V1 and perturbations in non-pilot input cause it to change to V2; Expected results: Observed aircraft thrust returns to value V1, respecting control objectives (settling time, overshoot, steady state error).
- UC5_TC_11 Preconditions: Aircraft is in operating mode M and system parameter P deviates at most +/- R % from nominal value; Input conditions / steps: Observed aircraft thrust is at value V1 and pilot input changes from A1 to A2; Expected results: Observed aircraft thrust changes and settles to value V2, respecting operating limit objectives (e.g., upper limit in shaft speed).
- UC5_TC_12 Preconditions: Aircraft is in operating mode M and system parameter P deviates at most +/- R % from nominal value; Input conditions / steps: Observed aircraft thrust is at value V1 and perturbations in non-pilot input cause it to change to V2; Expected results: Observed aircraft thrust returns to value V1, respecting operating limit objectives (e.g., upper limit in shaft speed).
- UC5_TC_13 Preconditions: Aircraft is in operating mode M; Input conditions / steps: Observed aircraft thrust is at value V1, pilot input changes from A1 to A2, and outside air pressure abruptly changes from P1 to P2; Expected results: Observed aircraft thrust changes and settles to value V2, respecting control objectives (settling time, overshoot, steady state error).
- UC5_TC_14 Preconditions: Aircraft is in operating mode M; Input conditions / steps: Observed aircraft thrust is at value V1, small perturbations in non-pilot input cause it to change to V2, and outside air pressure abruptly changes from P1 to P2; Expected results: Observed aircraft thrust returns to value V1, respecting control objectives (settling time, overshoot, steady state error).
- UC5_TC_15 Preconditions: Aircraft is in operating mode M; Input conditions / steps: Observed aircraft thrust is at value V1, pilot input changes from A1 to A2, and outside air pressure abruptly changes from P1 to P2; Expected results: Observed aircraft thrust changes and settles to value V2, respecting operating limit objectives (e.g., upper limit in shaft speed).
- UC5_TC_16 Preconditions: Aircraft is in operating mode M; Input conditions / steps: Observed aircraft thrust is at value V1, small perturbations in non-pilot input cause it to change to V2, and outside air pressure abruptly changes from P1 to P2; Expected results: Observed aircraft thrust returns to value V1, respecting operating limit objectives (e.g., upper limit in shaft speed).
- UC5_TC_17 Preconditions: Aircraft is in nominal operating mode; Input conditions / steps: Pilot input changes from A1 to A2, causing surge / stall avoidance indicator signal to be set; Expected results: Aircraft switches to surge / stall prevention operating mode.
- UC5_TC_18 Preconditions: Aircraft is in surge / stall prevention operating mode; Input conditions / steps: Pilot input changes from A1 to A2, causing surge / stall avoidance indicator signal to be cleared; Expected results: Aircraft switches to nominal operating mode.
- UC5_TC_19 Preconditions: Aircraft is in nominal operating mode; Input conditions / steps: Perturbations in non-pilot input cause surge / stall avoidance indicator signal to be set; Expected results: Aircraft switches to surge / stall prevention operating mode.
- UC5_TC_20 Preconditions: Aircraft is in surge / stall prevention operating mode; Input conditions / steps: Perturbations in non-pilot input cause surge / stall avoidance indicator signal to be cleared; Expected results: Aircraft switches to nominal operating mode.
- UC5_R_1 Under sensor faults, while tracking pilot commands, control objectives shall be satisfied.
- UC5_R_2 Under sensor faults, during regulation of nominal system operation, control objectives shall be satisfied.
- UC5_R_3 Under sensor faults, while tracking pilot commands, operating limit objectives shall be satisfied.
- UC5_R_4 Under sensor faults, during regulation of nominal system operation, operating limit objectives shall be satisfied.
- UC5_R_5 Under mechanical fatigue conditions, while tracking pilot commands, control objectives shall be satisfied.
- UC5_R_6 Under mechanical fatigue conditions, during regulation of nominal system operation, control objectives shall be satisfied.
- UC5_R_7 Under mechanical fatigue conditions, while tracking pilot commands, operating limit objectives shall be satisfied.
- UC5_R_8 Under mechanical fatigue conditions, during regulation of nominal system operation, operating limit objectives shall be satisfied.
- UC5_R_9 Under low probability hazardous events, while tracking pilot commands, control objectives shall be satisfied.
- UC5_R_10 Under low probability hazardous events, during regulation of nominal system operation, control objectives shall be satisfied.
- UC5_R_11 Under low probability hazardous events, while tracking pilot commands, operating limit objectives shall be satisfied.
- UC5_R_12 Under low probability hazardous events, during regulation of nominal system operation, operating limit objectives shall be satisfied.
- UC5_R_13 While tracking pilot commands, controller operating mode shall appropriately switch between nominal and surge / stall prevention operating state.
- UC5_R_14 During regulation of nominal system operation, controller operating mode shall appropriately switch between nominal and surge / stall prevention operating state.