Information Technology Reference
In-Depth Information
Step 1.
Oine Analysis & Powerset Construction.
In this step, a sanity check
of whether a system property violation occurs is first performed. If not,
then there is no need for the causality analysis. Otherwise, we check
Hypothesis 1 defined in Subsection 2.2. When Hypothesis 1 holds, we
gather the set
of faulty components for the violation of
ϕ
S
on trace
Tr
, and construct the powerset 2
F
of
F
.
Step 2.
Trace Reconstruction.
The trace reconstruction for the causality analysis
is based on the system specification, and parametric to the suspected
subset
F
of faulty components and the causality definition. This
step is at the core of the causality analysis, and we will discuss it in
Section 4.
Step 3.
Causality Analysis & Collecting Causes.
For each suspected subset
C⊆F
C⊆
F
is a
culprit according to the chosen causality definition
CD
.Ifyes,itis
collected for the subsequent culprit minimization; otherwise
of faulty components, the causality analysis checks whether
C
is not a
cause for the violation of system property
ϕ
S
according to
CD
.
Step 4.
Culprit Minimization.
The last step of causality analysis is to check
the minimality of each collected culprit, according to Definition 4. Non-
minimal culprits are pruned for precise results of causality analysis.
C
4 Trace Reconstruction and Causality Analysis
The trace reconstruction step in the causality analysis is to identify the set
TR
C
of traces when the suspected subset
of faulty tasks in system
S
are replaced
with correct ones and the system is rerun with the same input as observed on
trace
Tr
. The main idea in obtaining
TR
C
is to specify the logical constraint
ψ
that exactly the traces in
TR
C
satisfy. The constraint
ψ
is composed based
on (1) task constraints for correct tasks, (2) tasks constraints for faulty tasks,
(3) constraints on values observed on trace
Tr
,and(4)
trace reconstruction rules
.
With the constructed logical constraint
ψ
, the problem of checking of causality
based on Definition 8 (Definition 9, resp.) can be transformed into the problem
of satisfiability (unsatisfiability, resp.) checking, for which state-of-the-art solvers
exist [26].
In this section, we show the extension of the work presented in [26] to the case
where real-time systems are considered, i.e., traces are sequences of timestamped
events as in Definition 1, and system/task specifications are given as logical
constraints in either temporal logics or first order logic on events.
Given a causality analysis problem instance
C
S,ϕ
S
,Tr,CD
, Step 1 of the
causality analysis framework is to identify the set
of faulty tasks according to
Definition 2. In Step 2, for each non-empty suspected subset
F
C⊆F
,aset
TR
C
of system traces is reconstructed, given that the faulty tasks in
are replaced
with good ones and the system
S
is rerun with the same input events. Each
task's behavior in the system is determined by the trace reconstruction rules,
which indicate what constraint must be put on each task
C
j
in
S
, according to
whether the task is (1) non-faulty, (2) faulty but not suspected, and (3) faulty
and suspected. Informally, the three rules are summarized as follows.
C
