-
Notifications
You must be signed in to change notification settings - Fork 1
/
MiniTownInfinite.smv
113 lines (95 loc) · 2.68 KB
/
MiniTownInfinite.smv
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
MODULE tank
VAR
height:real;
------------------
MODULE pump
VAR
status:{on,off};
------------------
MODULE control_system
VAR
tank_sensor:real;
actuator1:{on,off};
actuator2:{on,off};
ASSIGN
next(actuator1) := case
next(tank_sensor) <= 400 : on;
next(tank_sensor) >= 630 : off;
TRUE : actuator1;
esac;
next(actuator2) := case
next(tank_sensor) <= 100 : on;
next(tank_sensor) >= 450 : off;
TRUE : actuator2;
esac;
------------------
MODULE main
VAR
p1:pump;
p2:pump;
t:tank;
cs:control_system;
demand:real;
plc_pump_link: {secure,compromised};
plc_tank_link: {secure,compromised};
type_attack: {none,sensor,actuator,any};
DEFINE
pumpFlow0 := 0;
pumpFlow1 := 113.699 + 6.735*demand - 1.35* (t.height/100);
pumpFlow2 := 181.44 + 18.356*demand - 2.1*(t.height/100);
tankFlow0 := demand * 246 - pumpFlow0;
tankFlow1 := demand * 246 - pumpFlow1;
tankFlow2 := demand * 246 - pumpFlow2;
dT0 := tankFlow0 * 0.004678 *100;
dT1 := tankFlow1 * 0.004678 *100;
dT2 := tankFlow2 * 0.004678 *100;
ASSIGN
init(type_attack) := none; -- change as needed
next(type_attack) := type_attack;
init(plc_pump_link) := secure;
init(plc_tank_link) := secure;
init(t.height) := 500;
init(cs.tank_sensor) := 500;
init(p1.status) :=on;
init(p2.status) :=off;
init(cs.actuator1) :=on;
init(cs.actuator2) :=off;
next(plc_pump_link) := case
type_attack = actuator:compromised;
type_attack = any:compromised;
TRUE: secure;
esac;
next(plc_tank_link) := case
type_attack = sensor:compromised;
type_attack = any:compromised;
TRUE: secure;
esac;
next(p1.status) := case
plc_pump_link = secure:next(cs.actuator1);
TRUE:{on,off};
esac;
next(p2.status) := case
plc_pump_link = secure:next(cs.actuator2);
TRUE:{on,off};
esac;
TRANS plc_tank_link = secure -> next(cs.tank_sensor) = next(t.height);
TRANS plc_tank_link = compromised -> next(cs.tank_sensor) >= 0;
-- the physics
TRANS p1.status = off & p2.status = off -> next(t.height) = t.height - dT0;
TRANS p1.status = on & p2.status = off -> next(t.height) = t.height - dT1;
TRANS p1.status = on & p2.status = on -> next(t.height) = t.height - dT2;
TRANS p1.status = off & p2.status = on -> next(t.height) = t.height - dT1;
--INVAR t.height - cs.tank_sensor <= 50;
--INVAR t.height - cs.tank_sensor >= -50;
INVAR demand <= 1;
INVAR demand >= 0;
LTLSPEC G (t.height <= 400); -- 0
LTLSPEC G (t.height <= 550); -- 1
LTLSPEC G (t.height <= 600); -- 2
LTLSPEC G (t.height <= 650); -- 3
LTLSPEC G (t.height >= 300); -- 4
LTLSPEC G (t.height >= 200); -- 5
LTLSPEC G (t.height >= 100); -- 6
LTLSPEC G (t.height >= 25); -- 7
LTLSPEC G (t.height >= 10); -- 8
LTLSPEC G (t.height >= 0); -- 9