Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / tests / cocospec / FSMAutopilotSpec.lus @ f470cec6

History | View | Annotate | Download (2.42 KB)

1
contract FSM_AutopilotSpec(apfail:bool; good:bool; prevState:real; standby:bool; supported:bool; ) returns (pullup:bool; state_1:real; );
2

    
3
--Block Path: fsm_12B/FiniteStateMachine/Manager
4

    
5
let
6
var FTP:bool = true -> false;
7

    
8

    
9

    
10
--valid
11
guarantee "FSM002" S( (((standby and prevState = 0.0) => (state_1 = 3.0)) and FTP), ((standby and prevState = 0.0) => (state_1 = 3.0)) );
12

    
13

    
14
--guarantee "FSM003" S( (((prevState = 0.0 and good and supported) => (state_1 = 1.0)) and FTP), ((prevState = 0.0 and good and supported) => (state_1 = 1.0)) );
15
--the reuirement is not correct as they didn't clearly mentionned the pilot is not in control (not standby).
16
-- the correct version should be 
17
-- "3.	The autopilot shall change states from TRANSITION to NOMINAL when the pilot is not in control and the system is supported and sensor data is good.
18
guarantee "FSM003V2" prevState = 0.0 and not standby and good and supported => state_1 = 1.0;
19

    
20

    
21
--guarantee "FSM008" S( (((prevState = 3.0 and not standby) => (state_1 = 0.0)) and FTP), ((prevState = 3.0 and not standby) => (state_1 = 0.0)) );
22
-- the requirement is not correct, they forgot to mention "a failure does not occur (not apfail)" 
23
guarantee "FSM008V2" prevState = 3.0 and not standby and not apfail => state_1 = 0.0;
24

    
25
--valid
26
guarantee "FSM009" S( (((prevState = 3.0 and apfail) => (state_1 = 2.0)) and FTP), ((prevState = 3.0 and apfail) => (state_1 = 2.0)) );
27

    
28

    
29
--valid
30
guarantee "FSM005" S( (((prevState = 1.0 and standby) => (state_1 = 3.0)) and FTP), ((prevState = 1.0 and standby) => (state_1 = 3.0)) );
31

    
32
--guarantee "FSM007" S( (((pullup and supported and good) => (state_1 = 0.0)) and FTP), ((pullup and supported and good) => (state_1 = 0.0)) );
33
-- the formalization is not correct. In the table in definition of pullup: "True when the autopilot is in the MANEUVER state"
34
-- the requirement is also not correct as it did not mentioned "not standby".
35
guarantee "FSM007V2" prevState = 2.0 and supported and good and not standby => (state_1 = 0.0) ;
36

    
37

    
38
--guarantee "FSM004" S( (((not good and prevState = 1.0) => (state_1 = 2.0)) and FTP), ((not good and prevState = 1.0) => (state_1 = 2.0)) );
39
-- the requirement is also not correct as it did not mentioned "not standby".
40
guarantee "FSM004V2" not good and prevState = 1.0 and not standby => state_1 = 2.0;
41

    
42
--valid
43
guarantee "FSM006" S( (((prevState = 2.0 and standby and good) => (state_1 = 3.0)) and FTP), ((prevState = 2.0 and standby and good) => (state_1 = 3.0)) );
44

    
45

    
46

    
47

    
48

    
49
tel