Information Technology Reference
In-Depth Information
(R1) If
C
j
∈F
, then it is deemed as a good task. In the trace reconstruction,
C
j
's behavior is constrained by
ϕ
C
j
, i.e., a correct task's constraint.
(R2) If
C
j
∈F\C
, i.e.,
C
j
is faulty but not in the consideration of being
suspected, then all output events produced by
C
j
on trace
Tr
are preserved
on any reconstructed traces.
(R3) If
C
j
∈C⊆F
,then
C
j
is a faulty task that is replaced by a good one. In
this case, the trace reconstruction “removes” the events that should not
haveoccurredonthetrace
Tr
, and “adds” those which must be produced
by
C
j
.
The logical constraint to express that an event
e
is observed at time
t
on the
trace
Tr
is expressed as
(
e
,t
)
Tr.e
=
e
t
=
t.
on
Tr
(
e,t
):=
∃
∈
∧
(5)
The constraint that all events task
C
j
produced on
Tr
are preserved on re-
constructed traces is specified with
(
e
,t
)
.e
=
e
t
=
t
]
.
κ
C
j
:=
∀
e
∈
O
C
j
.
∀
t
∈
R
≥
0
.
[
on
Tr
(
e,t
)
→∃
∧
(6)
The constraint
κ
C
j
means that, any execution trace that satisfies
κ
C
j
must
have an event
e
which is the same as the
e
delivered at time
t
=
t
, for any
timestamped event (
e,t
)on
Tr
.
The task constraint of “removing” events from a trace in the trace reconstruc-
tion is done by adding more constraints to rule out traces where the events that
have to be removed occur. An event
e
must be removed in the trace reconstruc-
tion if (1)
e
is produced by a suspected faulty task
C
j
, and (2) there is no other
event on the trace that triggers the event
e
. The task constraint of “adding”
events that a faulty task
C
j
must have produced is specified by augmenting the
task constraint
ϕ
C
j
to specify the allowed time ranges for output events from
C
j
. The definitions of the “removing” and “adding” constraints are application
dependent. We defer the details to Subsection 5.3, and use
ρ
C
j
and
α
C
j
for now
to represent the two constraints for “removing” and “adding”, respectively.
The conditions for the rules (R1)-(R3) are defined as
ξ
C
j
,
1
:=
¬
in
(
C
j
,
F
)
.
(7)
ξ
C
j
,
2
:=
in
(
C
j
,
F
)
∧¬
in
(
C
j
,
C
)
.
(8)
ξ
C
j
,
3
:=
¬
in
(
C
j
,
C
)
.
(9)
):=
C∈F
Here the
in
is the set membership relation defined as
in
(
C
j
,
C
=
C
j
.
The task constraint for
C
j
in the trace reconstruction is then specified as
F
⎧
⎨
ϕ
C
j
,
if
ξ
C
j
,
1
,
ψ
C
j
:=
κ
C
j
,
if
ξ
C
j
,
2
,
(10)
⎩
α
C
j
∧
ρ
C
j
,
if
ξ
C
j
,
3
.
Finally, it is required that exactly the set of observed system input events
on
Tr
occur in reconstructed traces. The set
I
of possible system input
