Information Technology Reference
In-Depth Information
events is application dependent. For example, for the GPCA case study,
I
=
{
enq(Q1, bolus), enq(Q1, empty), enq(Q1, non-empty)
}
. This constraint
is defined as
!(
e
,t
)
.e
=
e
t
=
t
]
.
ι
:=
∀
e
∈
I.
∀
t
∈
R
≥
0
.
[
on
Tr
(
e,t
)
↔∃
∧
(11)
! quantifier means “there exists one and only one.” The behavior
of the reconstructed system is then specified with the formula
Here, the
∃
ψ
:=
ι
∧
ψ
C
1
∧
...ψ
C
J
.
(12)
Proposition 1.
The formula
ψ
defined in Equation
(12)
defines the set
TR
C
of the possible system behaviors with the same input as observed on
Tr
,after
suspected tasks in
C
are replaced with correct ones. That is,
TR
C
=
{tr | tr |
=
ψ}
.
The construction in this section is a combination of Steps 2 and 3 in the
causality analysis framework (cf. Figure 2) for a given suspected faulty subset
C
. The formula
ψ
in Equation (12) characterizes the set of reconstructed traces,
whereas the satisfiability (unsatisfiability, resp.) result corresponds to whether
the subset
is a cause with respect to Definition 8 (Definition 9, resp.). Due to
Proposition 1, to check that the subset
C
C
is a cause according to Definition 8,
it suces to check that
ψ
∧
ϕ
S
is satisfiable. To check that the subset
C
is a
cause according to Definition 9, it suces to check that
ψ
ϕ
S
is unsatisfiable.
State-of-the-art SAT/SMT solvers, e.g., Z3 [7], can be leveraged in solving the
causality analysis problem, as shown in our previous work [26].
∧¬
5 The GPCA Case Study
Tabl e 3.
ASampleTraceforGPCA
In this section, we use the GPCA case
study to illustrate how the causality
analysis problem is solved. We first
show a few informal examples, then
the formal definitions of the GPCA
system, and finally the analysis using
the causality analysis framework and
trace reconstruction techniques from
Sections 3 and 4.
A sample trace we will analyze is
shown in Table 3. The ID column
is added for the convenience of ref-
erence. The Task column indicates
which task has produced the corre-
sponding event. The Time column is the timestamp for the corresponding event.
On this trace, a bolus request is detected at 8500 ms, and an infusion session
starts at 8702 ms. An empty reservoir is detected at 17000 ms, and an alarm is
raised at 17008 ms, together with a stop event from
AC
which ends the infusion
session. The stop event from
PM
does not affect the pump operation in this
case.
ID Task Event
Time (ms)
1
BR
enq(Q1, bolus)
8500
2
PI
deq(Q1, bolus)
8502
3
PI
enq(Q2, bolus)
8503
4
PM
deq(Q2, bolus)
8701
5
PM
start
8702
6
ER
enq(Q1, empty)
17000
7
PI
deq(Q1, empty)
17004
8
PI
enq(Q3, empty)
17005
9
AC
deq(Q3, empty)
17007
10
AC
alarm
17008
11
AC
stop
17008
12
PM
stop
17701
