Information Technology Reference
In-Depth Information
Tabl e 2.
Events Recorded in GPCA Controller
Event Task Description
start
PM
The pump motor has been started.
stop
PM
or
AC
The pump motor has been stopped.
alarm
AC
The alarm has been fired.
enq(q, m)
BR
,
ER
,or
PI
Messagem has been put to queue q.
deq(q, m)
PI
,
PM
,or
AC
Messagem has been retrieved from queue q.
The data flow of the events in the system is depicted in Figure 1. The Bolus-
Req (
BR
) and EmptyRsvDetection (
ER
) tasks periodically check if there are
patient bolus request or empty/non-empty reservoir signals from sensors, respec-
tively; if there are, they put the messages to Q1. We do not consider faults in
these two tasks in our analysis. The aperiodic PlatformIndependent (
PI
)taskis
triggered whenever there is a message sent to Q1. It moves the bolus request and
empty/non-empty reservoir messages to Q2 and Q3, respectively. The PumpMo-
torCtr (
PM
) task periodically checks if there are bolus request messages in Q2;
if there are, it will start the infusion session by keeping the pump motor running
for 30 periods (i.e., 9 seconds for each patient bolus request). The AlarmCtr
(
AC
) task periodically checks if there are empty reservoir messages in Q3; if
there are, it will raise an alarm and stop the pump motor. Each task has a
response time of 10 ms after a message is received. We assume here that the
queues in the system are reliable, i.e., no messages are lost/duplicated/altered
in a queue.
The task behaviors described above reflect our black-box assumption: the two
data flow paths shown in Figure 1 both pass through queue Q1 and the task
PI
,
yet we do not know whether there is fault propagation from the
EMPTY RSV
sensor to the
PM
task, due to the assumption that
PI
is a black-box to the
analysis. (The dashed links inside
PI
in Figure 1 indicate unknown data flows.)
Essentially, this is what we intend to infer from the causality analysis.
With the recorded events, we express the GPCA safety requirement as the
following Metric Interval Temporal Logic (MITL) [1] property:
ϕ
S
:=
(0
,∞
)
[enq(Q1, bolus)
→
♦
(0
,
650)
[start
∧
[
∨
[
(0
,
9000)
[enq(Q1,empty)
→
[
♦
(0
,
1050)
alarm
∧
♦
(0
,
1050)
stop]]]]]
.
(0
,
9000)
¬
enq(Q1, empty)
∧
♦
(8990
,
9010)
stop]
(1)
The values in the formula are obtained from the system implementation. For
example, the value 650, indicating the maximal allowed delay (in milliseconds)
from the instance when a bolus is put to Q1 to the instance when the start
message is delivered by
PM
, is due to that (a) the aperiodic task
PI
has a worst
case delay of 10 ms to retrieve the message bolus from Q1, plus a possible 10 ms
delay due to preemption by
PM
; (b) similarly a 20 ms worst case delay for
PI
to move the bolus message to Q2; (c) since
PM
has a period of 300 ms, in
the worst case, it takes up to two periods of
PM
to read the message once it is
enqueued in Q2 (see Figure 3 in Subsection 5.2 for details), and (d) the worst
