Project

General

Profile

Revision f470cec6

View differences:

tests/cocospec/FSMAutopilotSpec.lus
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
tests/cocospec/FSMSensorSpec.lus
1
contract FSM_SensorSpec(MODE:bool; limits:bool; prevSensState:real; request:bool; ) returns (sensState: real; );
2

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

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

  
8

  
9
--guarantee "FSM011" S( (((prevSensState = 0.0 and not request) => (sensState = 1.0)) and FTP), ((prevSensState = 0.0 and not request) => (sensState = 1.0)) );
10
-- This requirement is not correct as they did not mention "when limits are not exceeded" which is implicitly implicated from  "FSM010" requirement. 
11
-- To rewrtie it: "11.	The sensor shall change states from NOMINAL to TRANSITION when the autopilot is not requesting support and limits are not exceeded."
12
guarantee "FSM011V2" (prevSensState = 0.0 and not request and not limits) => (sensState = 1.0);
13

  
14

  
15
--valid
16
guarantee "FSM012" S( (((prevSensState = 2.0 and not request and not limits) => (sensState = 1.0)) and FTP), ((prevSensState = 2.0 and not request and not limits) => (sensState = 1.0)) );
17

  
18

  
19
--valid
20
guarantee "FSM010" S( (((prevSensState = 0.0 and limits) => (sensState = 2.0)) and FTP), ((prevSensState = 0.0 and limits) => (sensState = 2.0)) );
21

  
22

  
23
--valid
24
guarantee "FSM013" S( (((prevSensState = 1.0 and request and MODE) => (sensState = 0.0)) and FTP), ((prevSensState = 1.0 and request and MODE) => (sensState = 0.0)) );
25

  
26

  
27
tel
28

  
tests/cocospec/FSMSpec.lus
1
--Historically
2
node H(X:bool) returns (Y:bool);
3
let
4
    Y = X -> (X and (pre Y));
5
tel
6

  
7
--Y since inclusive X
8
node SI(X,Y: bool) returns (Z:bool);
9
let
10
Z = Y and (X or (false -> pre Z));
11
tel
12

  
13
--Y since X
14
node S(X,Y: bool) returns (Z:bool);
15
let
16
Z = X or (Y and (false -> pre Z));
17
tel
18

  
19
--Once
20
node O(X:bool) returns (Y:bool);
21
let
22
 Y = X or (false -> pre Y);
23
tel
24

  
25
node First( X : bool ) returns ( Y : bool );
26
let
27
  Y = X -> pre Y;
28
tel
29

  
30
--Timed Once: less than or equal to N
31
node OTlore(const N: int; X: bool; ) returns (Y: bool);
32
    var C:int;
33
let
34
    C = if X then 0
35
        else (-1 -> pre C + (if pre C <0 then 0 else 1));
36

  
37
    Y = First(X)
38
        ->
39
        (if pre C < 0  then false
40
         else C <= N
41
        );
42
tel
43

  
44
-- Timed Historically: less than or equal to N
45
node HTlore(const N: int; X: bool) returns (Y: bool);
46
let
47
  Y = not OTlore(N, not X);
48
tel
49

  
50
-- Timed Since: less than or equal to N
51
node STlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);
52
let
53
  Z = S(X, Y) and OTlore(N, X);
54
tel
55

  
56
-- Timed Since Inclusive: less than or equal to N
57
node SITlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);
58
let
59
  Z = SI(X,Y) and OTlore(N, X);
60
tel
61

  
62
contract FSMSpec(apfail:bool; limits:bool; standby:bool; supported:bool; ) returns (pullup: bool; );
63

  
64
--Block Path: fsm_12B
65

  
66
let
67

  
68
var FTP:bool = true -> false;
69

  
70
--guarantee "FSM001" S( (((limits and not standby and not apfail and supported) => (pullup)) and FTP), ((limits and not standby and not apfail and supported) => (pullup)) );
71
guarantee "FSM001V2" limits and not standby and not apfail and supported => pullup;
72

  
73
tel
74

  
tests/cocospec/TriplexSignalMonitorSpec.lus
1
--Historically
2
node H(X:bool) returns (Y:bool);
3
let
4
    Y = X -> (X and (pre Y));
5
tel
6

  
7
--Y since inclusive X
8
node SI(X,Y: bool) returns (Z:bool);
9
let
10
Z = Y and (X or (false -> pre Z));
11
tel
12

  
13
--Y since X
14
node S(X,Y: bool) returns (Z:bool);
15
let
16
Z = X or (Y and (false -> pre Z));
17
tel
18

  
19
--Once
20
node O(X:bool) returns (Y:bool);
21
let
22
 Y = X or (false -> pre Y);
23
tel
24

  
25
node First( X : bool ) returns ( Y : bool );
26
let
27
  Y = X -> pre Y;
28
tel
29

  
30
--Timed Once: less than or equal to N
31
node OTlore(const N: int; X: bool; ) returns (Y: bool);
32
    var C:int;
33
let
34
    C = if X then 0
35
        else (-1 -> pre C + (if pre C <0 then 0 else 1));
36

  
37
    Y = First(X)
38
        ->
39
        (if pre C < 0  then false
40
         else C <= N
41
        );
42
tel
43

  
44
-- Timed Historically: less than or equal to N
45
node HTlore(const N: int; X: bool) returns (Y: bool);
46
let
47
  Y = not OTlore(N, not X);
48
tel
49

  
50
-- Timed Since: less than or equal to N
51
node STlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);
52
let
53
  Z = S(X, Y) and OTlore(N, X);
54
tel
55

  
56
-- Timed Since Inclusive: less than or equal to N
57
node SITlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);
58
let
59
  Z = SI(X,Y) and OTlore(N, X);
60
tel
61

  
62
node abs(x:real)
63
returns(y:real);
64
let
65
	y = if x >= 0.0 then x else - x;
66
tel
67
node max(x1, x2:real)
68
returns(y:real);
69
let
70
	y = if x1 >= x2 then x1 else x2;
71
tel
72

  
73
node min(x1, x2:real)
74
returns(y:real);
75
let
76
	y = if x1 >= x2 then x2 else x1;
77
tel
78

  
79
node ToInt (X: bool) returns (N: int) ;
80
let
81
  N = if X then 1 else 0 ;
82
tel
83

  
84
node Count (X: bool) returns (N: int) ;
85
let
86
  N = ToInt(X) -> ToInt(X) + pre N ;  
87
tel
88

  
89
contract TriplexSignalMonitorSpec(Tlevel:real; ia:real; ib:real; ic:real; PCLimit: int; ) returns (FC: int; set_val: real; TC: int; PC: int);
90

  
91
--Block Path: triplex_12B
92

  
93
let
94
var FTP:bool = true -> false;
95
 var absAB: real = abs(ia - ib);
96
 var absAC: real = abs(ia - ic);
97
 var absBC: real = abs(ib - ic);
98
 var avg: real = (ia + ib + ic) / 3.0;
99
 var mid_value:real = if (abs(ia - avg) > abs(ic - avg) and abs(ib - avg) > abs(ic - avg)) then ic 
100
                      else if (abs(ia - avg) > abs(ib - avg)) then ib 
101
                      else ia;
102
var preFC: int = 0 -> pre FC;
103
var prePC: int = 0 -> pre PC;
104
var prePCLimit: int = 0 -> pre PCLimit;
105
var prevSet_val: real = 0.0 -> pre set_val;
106
-- calculate is_a_miscompare 
107
var C1:bool = absAB > Tlevel;
108
var C2:bool = absBC > Tlevel;
109
var C3:bool = absAC > Tlevel;
110
var is_a_miscompare : bool =  (not C1 and C2 and C3)  or (C1 and not C2 and C3) or (C1 and C2 and not C3);
111

  
112
-- Assumptions
113
assume PCLimit > 0 ;
114
assume true -> PCLimit = prePCLimit;
115
assume true -> Tlevel = pre Tlevel;
116

  
117
-- when preFC = 0 & prePC > prePCLimit TriplexSignalMonitor shall immediately satisfy FC > 0
118
--guarantee "RM001" S( (((preFC = 0 and prePC > prePCLimit) => (FC > 0)) and FTP), ((preFC = 0 and prePC > prePCLimit) => (FC > 0)) );
119
--guarantee "RM001V2" is_a_miscompare and prePC > PCLimit => FC > 0;
120

  
121
-- when FC =1 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ia +ib)
122
--guarantee "RM003a" (S( (( not (FC = 1)) and FTP), ( not (FC = 1)) )) or (S( ((set_val = 0.5 * ( ia + ib )) and ((FC = 1) and (FTP or (pre (S( (( not (FC = 1)) and FTP), ( not (FC = 1)) )))))), (set_val = 0.5 * ( ia + ib )) ));
123
--guarantee "RM003aV2" FC = 1 => set_val = 0.5 * (ia +ib);
124

  
125
-- when FC =2 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ia +ic).
126
--guarantee "RM003b"  (S( (( not (FC = 2)) and FTP), ( not (FC = 2)) )) or (S( ((set_val = 0.5 * ( ia + ic )) and ((FC = 2) and (FTP or (pre (S( (( not (FC = 2)) and FTP), ( not (FC = 2)) )))))), (set_val = 0.5 * ( ia + ic )) ));
127
--guarantee "RM003bV2" FC = 2 => set_val = 0.5 * (ia +ic);
128

  
129

  
130
-- when FC =4 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ib +ic)
131
--guarantee "RM003c" (S( (( not (FC = 4)) and FTP), ( not (FC = 4)) )) or (S( ((set_val = 0.5 * ( ib + ic )) and ((FC = 4) and (FTP or (pre (S( (( not (FC = 4)) and FTP), ( not (FC = 4)) )))))), (set_val = 0.5 * ( ib + ic )) ));
132
--guarantee "RM003cV2" FC = 4 => set_val = 0.5 * (ib +ic);
133

  
134
-- when preFC =0 TriplexSignalMonitor shall immediately satisfy set_val = mid_value
135
--guarantee "RM002" S( (((preFC = 0) => (set_val = mid_value)) and FTP), ((preFC = 0) => (set_val = mid_value)) );
136
--guarantee "RM002V2" FC = 0 => set_val = mid_value;
137

  
138
-- when (absAB > Tlevel & absAC >Tlevel) | (absAB > Tlevel & absBC > Tlevel) | (absAC > Tlevel & absBC > Tlevel) TriplexSignalMonitor shall always satisfy set_val = prevSet_val
139
--guarantee "RM004" (S( (( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) and FTP), ( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) )) or (S( ((set_val = prevSet_val) and ((( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel )) and (FTP or (pre (S( (( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) and FTP), ( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) )))))), (set_val = prevSet_val) ));
140

  
141
--Explanaton from document: 
142
--    -A miscompare that persists but has not yet been declared failed is known as a failure in progress.
143
--       can be expressed as "is_a_miscompare and prePC > 0 and prePC < PCLimit"
144
--    -A second failure can be expressed as "Count(FC > 0) = 1"
145
--[RM-004] If a second failure is in progress, the selected value shall remain unchanged from the previous selected value.
146
guarantee "RM004V2"  Count(FC > 0) = 1   and is_a_miscompare and prePC > 0 and prePC < PCLimit => set_val = prevSet_val;
147

  
148
--guarantee true ->   Count(FC > 0) = 1  and ia <> pre ia and ib <> pre ib  and ic <> pre ic  and prePC > 0  and prePC < PCLimit => set_val   <> prevSet_val;
149
tel
tests/cocospec/integrator_12BWithoutModesAndInitialization.lus
1
--Historically
2
node H(X:bool) returns (Y:bool);
3
let
4
    Y = X -> (X and (pre Y));
5
tel
6

  
7
--Y since inclusive X
8
node SI(X,Y: bool) returns (Z:bool);
9
let
10
Z = Y and (X or (false -> pre Z));
11
tel
12

  
13
--Y since X
14
node S(X,Y: bool) returns (Z:bool);
15
let
16
Z = X or (Y and (false -> pre Z));
17
tel
18

  
19
--Once
20
node O(X:bool) returns (Y:bool);
21
let
22
 Y = X or (false -> pre Y);
23
tel
24

  
25
node First( X : bool ) returns ( Y : bool );
26
let
27
  Y = X -> pre Y;
28
tel
29

  
30
--Timed Once: less than or equal to N
31
node OTlore(const N: int; X: bool; ) returns (Y: bool);
32
    var C:int;
33
let
34
    C = if X then 0
35
        else (-1 -> pre C + (if pre C <0 then 0 else 1));
36

  
37
    Y = First(X)
38
        ->
39
        (if pre C < 0  then false
40
         else C <= N
41
        );
42
tel
43

  
44
-- Timed Historically: less than or equal to N
45
node HTlore(const N: int; X: bool) returns (Y: bool);
46
let
47
  Y = not OTlore(N, not X);
48
tel
49

  
50
-- Timed Since: less than or equal to N
51
node STlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);
52
let
53
  Z = S(X, Y) and OTlore(N, X);
54
tel
55

  
56
-- Timed Since Inclusive: less than or equal to N
57
node SITlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);
58
let
59
  Z = SI(X,Y) and OTlore(N, X);
60
tel
61

  
62
contract integrator_12BSpec(BL:real; ic:real; reset:bool; T:real; TL:real; xin:real; ) returns (yout: real; );
63

  
64
--Block Path: integrator_12B
65

  
66
let
67
var FTP:bool = true -> false;
68
var xinpv: real = 0.0 -> pre xin;
69
var ypv: real = 0.0 -> pre yout;
70
var normal: bool = not reset and yout <= TL and yout >= BL;
71
var normal_yout : real = T * 0.5 * ( xin + xinpv ) + ypv;
72
assume BL <=  TL;
73
--assume T > 0.0;
74
guarantee "TUI-002" S( ((yout <= TL and yout >= BL) and FTP), (yout <= TL and yout >= BL) );
75

  
76
guarantee "TUI-001" S((( BL <= ic and ic <= TL ) and reset) => (yout = ic) , (((( BL <= ic and ic <= TL ) and reset) => (yout = ic)) and FTP));
77

  
78
guarantee "TUI-003-V2" normal and ((normal_yout <= TL and normal_yout >= BL)) => yout = normal_yout;
79
--guarantee "TUI-003" true -> (H(((( not normal) and (pre ( normal ))) and ( not FTP)) => (pre (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) ))))) and ((S( (( not (( not normal) and (pre ( normal )))) and (normal and (FTP or (pre (  not normal ))))), ( not (( not normal) and (pre ( normal )))) )) => (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) )));
80

  
81

  
82
tel

Also available in: Unified diff