Information Technology Reference
In-Depth Information
, the formula ψ in Equation (12) is
constructed according to the Equations (5) through (12) and information from S ,
Tr ,
C⊆F
In Step 2, for each non-empty subset
C
F
. We now discuss the construction for the two application dependent
constraints ρ C j and α C j not discussed in Section 4.
Defining “Removing” and “Adding” Constraints. As discussed in Sec-
tion 4, one condition for an event to be removed from a trace is that it is not
triggered by any other events. The trigger relation between timestamped input
and output for a task is derived from the task's constraint. For example, the
constraint for AC specifies that the stop event and alarm event must be de-
livered within 10 ms once the enq(Q3, empty) event is read from queue Q3,
as defined in Equation (13). In this case, the trigger relation is expressed as
trig AC := { ((deq(Q3, empty) ,t ) , (stop ,t )) |
and
for all t ≤ t +10 }
(22)
∪{ ((deq(Q3, empty) ,t ) , (alarm ,t )) |
for all t ≤ t +10 }.
Similarly, the trigger relations for PI and PM are defined as follows.
trig PI := { ((deq(Q1, bolus) ,t ) , (enq(Q2, bolus) ,t )) |∀t ≤ t +10 }
∪{ ((deq(Q1, empty) ,t ) , (enq(Q3, empty) ,t )) |∀t ≤ t +10 }
∪{ ((deq(Q1, non-empty) ,t ) , (enq(Q3, non-empty) ,t )) |∀t ≤ t +10 }.
(23)
trig PM := { ((deq(Q3, empty) ,t ) , (start ,t )) |∀t ≤ t +10 }. (24)
The constraint for traces where the events produced by a faulty task C j are
removed is specified with
ρ C j := ∀e ∈ O C j .∀t ∈ R 0 . [[ ¬∃ ( e ,t ) . (( e ,t ) , ( e,t )) ∈ trig C j ]
¬∃ ( e ,t ) .e = t ∧ t = t ] .
(25)
Informally, this constraint means that if there is no trigger for event e at time
t , then it should not occur on any reconstructed traces.
For “adding” events to a trace, a task must only deliver output events when it
is activated by the FreeRTOS scheduler. This piece of information is unavailable
to oine analysis. We assume that the FreeRTOS scheduler would schedule each
task the same as on the observed trace Tr . The instance at which an event can
be produced on a reconstructed trace is then limited both by the task response
time and its activation time. For example, if AC reads the empty message at
time 8701 ms, and it is observed on Tr that AC is active in time ranges [8700 ms,
8703 ms], [8709 ms, 8712 ms], etc., then in addition to the 10 ms deadline to
deliver the events alarm and stop in the range [8701 ms, 8711 ms], AC can
only produce the events during the ranges of [8701 ms, 8703 ms] or [8709 ms,
8711 ms]. The constraint for this requirement is obtained by augmenting the task
constraint with the time information. For example, for AC , the specification is
α AC := γ AC ∧∀ ( e, t ) . [ e = deq(Q3, empty) →∃ ( e 1
i
,t 1
i
) , ( e 1
o
,t 1
o
) , ( e 2
i
,t 2
i
) , ( e 2
o
,t 2
o
) ∈ Tr.
[ e 1
i
= e 2
i
= in( AC ) ∧ e 1
o
= e 2
o
= out( AC ) ∧ t ≤ t 1
o ∧ t ≤ t 2
o
¬∃ ( e i ,t i ) , ( e o ,t o ) ∈ Tr. [[ e i = in( AC ) ∧ t 1
i
<t i ≤ t 1
o
] [ e o = out( AC ) ∧ t 1
i ≤ t o <t 1
o
]]
(26)
¬∃ ( e i ,t i ) , ( e o ,t o ) ∈ Tr. [[ e i = in( AC ) ∧ t 2
i
<t i ≤ t 2
o
] [ e o = out( AC ) ∧ t 2
i ≤ t o <t 2
o
]]]
!( e 1 ,t 1 ) . [ e 1 = stop [max( t, t 1
i
) ≤ t 1
min( t +10 ,t 1
o
)]]
!( e 2 ,t 2 ) . [ e 1 = alarm [max( t, t 2
i
) ≤ t 2
min( t +10 ,t 2
o
)]]] .
 
Search WWH ::




Custom Search