Information Technology Reference
In-Depth Information
case delay of the
PM
task is 10 ms. The rest of the time periods are analogously
specified. It is required that the behaviors of the tasks constitute a subset of the
behaviors specified by the system constraint
ϕ
S
, which is formally stated later
in Hypothesis 1 in Subsection 2.2.
A system execution is captured by collecting the events with their timestamps
by instrumenting the GPCA implementation. We assume in this paper that
recording is perfect, i.e., no events in the system are missing on a trace, and
each event on a trace actually happened at its recorded timestamp.
A trace is a set of timestamped events. For example,
(enq(Q1, bolus)
,
8500), (deq(Q1, bolus)
,
8502), (enq(Q3, empty)
,
8503), (deq(Q3, empty)
,
8701), (alarm
,
9760), (stop
,
9760)
{
is a trace with six events observed. The
events are naturally ordered by their corresponding timestamps. On this trace,
PI
mistakenly put the bolus request message to the wrong queue with the wrong
message.
AC
reads the empty reservoir message but fails to alarm and stop
within its deadline. The system property
ϕ
S
is violated since there is no bolus
dose delivered to the patient after the bolus request event enq(Q1, bolus) (i.e.,
Equation (1)). So two faulty tasks,
PM
and
AC
, may have caused the system
property violation.
In the causality analysis problem, we would like to investigate which subset
of the faulty tasks,
}
, caused the system property vio-
lation. We leave the details of the analysis to Section 5 but only show the result
here: both
{
PI
}
,
{
AC
}
,or
{
PI,AC
}
{
PI
}
and
{
PI,AC
}
satisfy the counterfactual test for causality, so we
report the minimal subset
{
PI
}
as the cause for the system property violation.
2.2 The Causality Analysis Problem Definition
In this subsection, we abstract the problem illustrated by the example in Sub-
section 2.1 and provide the formal definition of the
causality analysis problem
.
Definition 1
(Trace)
.
A
trace
of length
n
is a set of
n
timestamped events,
denoted
t
n
.
A trace only contains a finite number of events. For time beyond
t
n
,noevents
happen in the system. We use logical formula to express component/system
behaviors. It is assumed that given a trace
Tr
, the semantics of the chosen logic
is two-valued: for any formula
φ
, either
Tr
{
(
e
1
,t
1
)
,...,
(
e
n
,t
n
)
}
, such that
t
1
≤···≤
=
φ
.Inthispaper,MITL
and first order logic (FOL) are used for component/system specifications.
Definition 2
(Constraint)
.
Given a set
E
of events, a
constraint
is a logical
formula defined on
E
.Indetails,forMITL,
E
is the set of atomic propositions;
for an event
e
|
=
φ
or
Tr
|
∈
E
,
(
Tr,t
)
|
=
e
if and only if
(
e,t
)
∈
Tr
.ForFOL,
E
is the set
of logical constants.
Definition 3
(Component)
.
A
component
C
=
is a tuple where
the
I
C
and
O
C
are its set of input and output, respectively, such that
I
C
∩
I
C
,O
C
,ϕ
C
O
C
=
∅
,
and
ϕ
C
is a constraint defined on
I
C
∪
O
C
.
The notion of the component input/output is general. In the GPCA case
study, the input and output for each component are the events it could receive
and send through the queues, respectively; in [26], the input and output are
values passing through component data ports.
