-
Notifications
You must be signed in to change notification settings - Fork 1
/
test_scenarios.lando
235 lines (190 loc) · 11.2 KB
/
test_scenarios.lando
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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
// Copyright 2021, 2022, 2023 Galois, Inc.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
// Scenarios are sequences of events. Scenarios document normal and
// abnormal traces of system execution.
// Test scenarios are scenarios that validate a system conforms to its
// requirements through runtime verification (testing). Each scenario
// is refined to a (possibly parametrized) runtime verification
// property. If a testbench is complete, then every path of a
// system's state machine should be covered by the its set of scenarios.
scenarios Self-Test Scenarios
Normal Self-Test Behavior 1a - Trip on Mock High Pressure Reading from that Pressure Sensor
The user selects 'maintenance' for an instrumentation division, the
division's pressure channel is set to 'normal' mode, the pressure
setpoint is set to a value v, the user simulates a pressure input to
that division exceeding v, the division generates a pressure trip.
Normal Self-Test Behavior 1b - Trip on Environmental High Pressure Reading from that Pressure Sensor
The user selects 'maintenance' for an instrumentation division, the
division's pressure channel is set to 'normal' mode, the pressure
setpoint is set to a value v, the division reads a pressure sensor
value division exceeding v, the division generates a pressure trip.
Normal Self-Test Behavior 2a - Trip on Mock High Temperature Reading from that Temperature Sensor
The user selects 'maintenance' for an instrumentation division, the
division's temperature channel is set to 'normal' mode, the
temperature setpoint is set to a value v, the user simulates a
temperature input to that division exceeding v, the division generates
a temperature trip.
Normal Self-Test Behavior 2a - Trip on Environmental High Temperature Reading from that Temperature Sensor
The user selects 'maintenance' for an instrumentation division, the
division's temperature channel is set to 'normal' mode, the
temperature setpoint is set to a value v, the division reads a
temperature sensor value division exceeding v, the division generates
a temperature trip.
Normal Self-Test Behavior 3a - Trip on Mock Low Saturation Margin
The user selects 'maintenance' for an instrumentation division, the
division's saturation channel is set to 'normal' mode, the saturation
margin setpoint is set to a value v, the user simulates pressure and
temperature inputs to that division such that the saturation margin is
below v, the division generates a saturation margin trip.
Normal Self-Test Behavior 3a - Trip on Environmental Low Saturation Margin
The user selects 'maintenance' for an instrumentation division, the
division's saturation channel is set to 'normal' mode, the saturation
margin setpoint is set to a value v, the division reads pressure and
temperature sensor values in that division such that the saturation
margin is below v, the division generates a saturation margin trip.
Normal Self-Test Behavior 4 - Vote on Every Possible Like Trip
The user selects 'maintenance' for each instrumentation division, the
user configures a subset of channels to place in active trip output.
Normal Self-Test Behavior 5a - Automatically Actuate All Mock Devices in Sequence
The user selects 'maintenance' for each instrumentation division, the
user places enough channels in 'active trip' to actuate a mock device.
Normal Self-Test Behavior 5b - Automatically Actuate All Hardware Devices in Sequence
The user selects 'maintenance' for each instrumentation division, the
user places enough channels in 'active trip' to actuate a hardware
device.
Normal Self-Test Behavior 6 - Manually Actuate Each Device in Sequence
The user manually actuates each device.
Normal Self-Test Behavior 7a - Select Maintenance Operating Mode for each Division
The user selects 'maintenance' mode for each instrumentation division
in sequence.
Normal Self-Test Behavior 7b - Select Normal Operating Mode for each Division
The user exits 'maintenance' mode for each instrumentation division in
sequence.
Normal Self-Test Behavior 8 - Perform Each Kind of Setpoint Adjustment
For each instrumentation division, the user provides a setpoint for
temperature, then the user provides a setpoint for pressure, then the
user provides a setpoint for saturation margin.
Normal Self-Test Behavior 9 - Configure Bypass of Each Instrument Channel in Sequence
For each instrumentation division, the user puts each channel in
'normal' and then 'bypass' mode.
Normal Self-Test Behavior 10 - Configure Active Trip Output State of Each Instrument Channel in Sequence
For each instrumentation division, the user puts each channel in
'trip' and then 'normal' mode.
Normal Self-Test Behavior 11 - Display Pressure Temperature and Saturation Margin
The user provides inputs for an instrumentation division, then the UI
displays the updated pressure, temperature and saturation margin.
Normal Self-Test Behavior 12 - Display Every Trip Output Signal State in Sequence
The user configures an instrumentation division in 'maintenance',
selects a channel and places it in 'trip', the UI displays the trip
state, the user places the channel in 'normal' mode, the UI displays
the trip state.
Normal Self-Test Behavior 13 - Display Indication of Every Channel in Bypass in Sequence
The user configures an instrumentation division in 'maintenance', the
user selects a channel and places it in bypass, the UI displays the
bypass state, the user places the channel in normal mode, the UI
displays the updated state.
Normal Self-Test Behavior 14 - Demonstrate Periodic Continual Self-test of Safety Signal Path
The system starts, eventually the UI displays that self test has run.
Normal Self-Test Behavior 15 - Full Self-Test
The system selects two instrumentation divisions and a device, the
system simulates inputs to the selected instrumentation divisions, the
system checks that the correct actuation signal would be sent to the
selected device.
// Exceptional behaviors are *predictable* system behaviors triggered
// by external environment affects. Examples include a CPU, OS,
// device, or network total or partial failure. E.g., CPU deadlock,
// out-of-memory errors, permanent store partial and total failures,
// lack of space in permanent store, partial and total network
// failures, device driver partial or total failures, etc.
// In our architecture, every part of the RTS system, and particularly
// every part of the instrumentation and sensing subsystem and every
// part of the actuation subsystem must be able to fail and the system
// must respond appropriately.
// This is not detectable
Exceptional Behavior 1a - Cause Actuator 1 to Fail
Manually actuate Actuator 1, the actuator fails, an error is indicated.
// This is not detectable
Exceptional Behavior 1b - Cause Actuator 2 to Fail
Manually actuate Actuator 2, the actuator fails, an error is indicated.
// This is not detectable
Exceptional Behavior 1c - Non-deterministically Cause an Actuator to Eventually Fail
Repeatedly manually actuate/de-actuate an Actuator, the actuator fails,
an error is indicated.
Exceptional Behavior 2a - Cause Temperature Sensor 1 to Fail
Instrumentation units 1 and 2 report temperature readings that are
inconsistent with Instrumentation units 3 and 4, the discrepancy is
indicated on the UI.
Exceptional Behavior 2b - Cause Temperature Sensor 2 to Fail
Instrumentation units 1 and 2 report temperature readings that are
inconsistent with Instrumentation units 3 and 4, the discrepancy is
indicated on the UI.
Exceptional Behavior 2c - Non-deterministically Cause a Temperature Sensor to Eventually Fail
Instrumentation units 1 and 2 report temperature readings that are
inconsistent with Instrumentation units 3 and 4, the discrepancy is
indicated on the UI.
Exceptional Behavior 3a - Cause Pressure Sensor 1 to Fail
Instrumentation units 1 and 2 report pressure readings that are
inconsistent with Instrumentation units 3 and 4, the discrepancy is
indicated on the UI.
Exceptional Behavior 3b - Cause Pressure Sensor 2 to Fail
Instrumentation units 1 and 2 report pressure readings that are
inconsistent with Instrumentation units 3 and 4, the discrepancy is
indicated on the UI.
Exceptional Behavior 3c - Non-deterministically Cause a Pressure Sensor to Eventually Fail
Temperature Sensor 1 or Temperature Sensor 2 report inconsistent
values, the discrepancy is indicated on the UI.
// Can be further refined, e.g.:
// Sensor values are read by Instrumentation Unit 1, the unit generates the wrong trip signal,
Exceptional Behavior 4a - Cause Instrumentation Unit 1 to Fail
Instrumentation unit 1 fails, self test indicates that a test has
failed.
// Can be further refined, e.g.:
// Sensor values are read by Instrumentation Unit 1, the unit generates the wrong trip signal,
Exceptional Behavior 4b - Cause Instrumentation Unit 2 to Fail
Instrumentation unit 2 fails, self test indicates that a test has
failed.
// Can be further refined, e.g.:
// Sensor values are read by Instrumentation Unit 1, the unit generates the wrong trip signal,
Exceptional Behavior 4c - Cause Instrumentation Unit 3 to Fail
Instrumentation unit 3 fails, self test indicates that a test has
failed.
// Can be further refined, e.g.:
// Sensor values are read by Instrumentation Unit 1, the unit generates the wrong trip signal,
Exceptional Behavior 4d - Cause Instrumentation Unit 4 to Fail
Instrumentation unit 4 fails, self test indicates that a test has
failed.
Exceptional Behavior 4e - Non-Deterministically Cause Instrumentation Unit to Eventually Fail
At least one instrumentation unit fails to generate the appropriate
trip signal, self test runs, self test indicates that a test has
failed.
Exceptional Behavior 5a - Cause Temperature Demultiplexor 1 to Fail
At least one of Instrumentation units 1 or 2 report temperature
readings inconsistent with instrumentation units 3 and 4.
Exceptional Behavior 5b - Cause Temperature Demultiplexor 2 to Fail
At least one of Instrumentation units 3 or 4 report temperature
readings inconsistent with instrumentation units 1 and 2.
Exceptional Behavior 5c - Cause Pressure Demultiplexor 1 to Fail
At least one of Instrumentation units 1 and 2 report pressure readings
inconsistent with instrumentation units 3 and 4.
Exceptional Behavior 5d - Cause Pressure Demultiplexor 2 to Fail
At least one of Instrumentation units 3 and 4 report pressure readings
inconsistent with instrumentation units 1 and 2.
Exceptional Behavior 5e - Cause a Temperature Demultiplexor to Eventually Fail
All instrumentation units report consistent temperature readings, a
demultiplexor fails, at least one of the instrumentation units reports
an inconsistent temperature reading.
Exceptional Behavior 5f - Cause a Pressure Demultiplexor to Eventually Fail
All instrumentation units report consistent temperature readings, a
demultiplexor fails, at least one of the instrumentation units reports
an inconsistent pressure reading.