-
Notifications
You must be signed in to change notification settings - Fork 0
/
FMERSoS.sm
180 lines (113 loc) · 3.82 KB
/
FMERSoS.sm
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
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
// FM-ERSoS CTMC MODEL stochastic action rates between CSs --> (CPS-IoT nodes) (local gateways) (ECU)
// and First Responders
ctmc
// Parcipating Architectural elements in a particular Mission M and configuration
const int N;
// Stochastic Action reates as Transition Rates (Tr).
//global op: bool;
const double tr1 = 0.5;
const double tr2 = 1.50;
const double tr3 = 1.0;
const double tr4 = 3.5;
const double tr5 = 5.5;
const double tr6 = 4.5;
const double tr7 = 8.5;
// system non-deterministic stochatic behavior.
module CPSHWF
// possible number of states
sa:[0..4] init 0 ;
[readhumidity] sa=0 -> tr1: (sa'=1); // get humidity data
[measurewindflow] sa=0 -> tr1: (sa'=2); // get windflow data
[sendsensordata] (sa=1 | sa =2) -> tr5: (sa'=3); // humidity and windflow data together
[askaboutlocation] sa=2 | sa= 1 -> tr3 :(sa'=4);
[] (sa=3)| (sa=4)-> tr1:(sa'=0); // loop through for continous data fetch
[] sa=3 -> tr1: (sa'=2);
[] sa=3 -> tr1: (sa'=1);
[] sa>1 -> sa*tr6: (sa'=sa-1); // At point in time exchange of information may fail.
// states transitions with actions
endmodule
module CPSFS
// possible number of states
sb:[1..6] init 1 ;
[observefire] sb=1 -> tr1: (sb'=2); // get fire data (This is optional to show the working of CPS-node)
[detectsmoke] sb=1 -> tr1: (sb'=3); // get smoke data
[tellaboutlocation] ( sa=2 | sb= 3 )-> tr3 :(sb'=5);
[sendsensordata] (sb=3 |sb=2) -> tr6: (sb'=4);
[] (sb=4) | (sb=5)-> tr1:(sb'=1);
[] (sb=4) -> tr2: (sb'=2);
[] (sb=4) -> tr2: (sb'=3);
[] sb>2 -> sb*tr6:(sb'=sb-1); // At point in time exchange of information may fail.
endmodule
module CPSLCS // Local control station Gateway
sc: [1..6] init 1;
[recievedata] (sc=1) -> tr5: (sc'=2); // recivesensordata
[] (sc= 2 & sa =4) | (sc= 2 & sb=4) -> tr5 :(sc'=3); // process inital sensor data from CPS- nodes
[] (sa= 4 | sb =5) -> tr5:(sc'=4); // do action for prediction of fire
[transmitdatatoECU] sc= 2 -> tr5: (sc'= 5);
[sendalertstoECU] sc=2 -> tr7: (sc' =6);
// states transitions with actions
endmodule
module CPSECU
// possible number of states
sd: [1..4] init 1 ;
[recievedata] (sd=1)& (sc= 5) ->tr4 : (sd'=2);
[generatealerts] sd=2 -> tr7: (sd'=3); // to first responders
[genertewarnings] sc=2 & sd=3 -> tr6: (sd'=4); // to first responders
// states transitions with actions
endmodule
label "Mission_M1_G1_Achieved" = sc=5;
label "Mission_M1_G2_Achieved" = sc=6;
label "CPSHWF_may_degrade" = sa= 0;
label "CPSFS_may_degrade" = sb= 1;
label "Mission_M2_Achieved" =(sd=3 | sd=4);
// The expected time taken before sending sensor data
rewards "Time_spent_in_any_state"
true : 1;
endrewards
// The expected time taken before sending sensor data
rewards "Sensordata"
[sendsensordata] true: 1;
endrewards
rewards "no_sensormessages"
[sendsensordata] true:30;
endrewards
rewards "RecieveData"
[recievedata] true:1;
endrewards
// number of messages sent to First responders at time instance T
//rewards "
//endrewards
// number of CPS nodes working at time T
rewards "cpsnodes"
true :100* (sa+sb+sc+sd)/N;
endrewards
rewards "DatatoECU"
//[transmitdatatoECU] true:50;
[sendalertstoECU] true:50;
endrewards
//module policeservice
// possible number of states
// states transitions with actions
//endmodule
//module EmeergencyService
// possible number of states
// states transitions with actions
//endmodule
//module FireFirghtingService
// possible number of states
// states transitions with actions
//endmodule
// Final states of the configurations representing mission accomplishmnets
//module Mission finalstates
//endmodule
//
//labels
// formulas
//rewards "timeforsending alerts"
//endrewards
//rewards "timeforsending alerts"
//endrewards
//rewards "timeforsending alerts"
//endrewards
//rewards "timeforsending alerts"
//endrewards