Information Technology Reference
In-Depth Information
5.2 Formal Definitions for GPCA System
We first define constraints
ϕ
AC
,
ϕ
PI
,and
ϕ
PM
for the three tasks that can fail.
We do not consider faults in
BR
and
ER
in this paper. The constraint for each
task consists of two parts:
(1) what would a task do when it reads a message from a queue, and
(2) when would a task read a message if there is one in the corresponding queue.
For Part (1), the
AC
task's constraint is specified with
τ
AC
:=
∀
(
e, t
)
.
[
e
= deq(Q3, empty)
→∃
!(
e
,t
)
.
[
e
= stop
∧ t
≤ t
+10]
∧
∃
!(
e
,t
)
.
[
e
= alarm
∧ t
≤ t
+10]]
.
(13)
It is interpreted as, as long as there is a deq(Q3, empty) event on the trace,
there must be a stop event within 10 ms and an alarm event within 10 ms.
Similarly, the
PI
task's constraint is specified with
!(
e
,t
)
.
[
e
= enq(Q2, bolus)
∧
t
≤
τ
PI
:=
∀
(
e, t
)
.
[[
e
= deq(Q1,bolus)
→∃
t
+10]]
∧
[
e
= deq(Q1, empty)
→∃
!(
e
,t
)
.
[
e
= enq(Q3, empty)
∧ t
≤ t
+10]]
∧
[
e
= deq(Q1, non-empty)
→∃
!(
e
,t
)
.
[
e
= enq(Q3, non-empty)
∧ t
≤ t
+ 10]]]
.
(14)
The
PM
task's constraint is specified with
!(
e
,t
)
.
[
e
= start
∧
t
≤
τ
PM
:=
∀
(
e, t
)
.
[
e
= deq(Q2,bolus)
→∃
∧
∃
!(
e
,t
)
.
[
e
= stop
∧
8990
≤ t
− t
≤
9010]]]
.
t
+10
(15)
For Part (2), the aperiodic task
PI
and the two periodic tasks
PM
and
AC
have different behaviors when a message the task should read is present in the
corresponding queue. In the GPCA implementation,
PI
is set to preempt lower
priority tasks to process the message and put it to the corresponding queues.
This behavior is specified with the constraint
γ
PI
in Equation (16). The value
20 ms is due to the possible preemption of
PI
by the even higher priority
PM
.
γ
PI
:=
∀
(
e, t
)
.
[[
e
= enq(Q1,bolus)
→∃
!(
e
,t
)
.
[
e
= deq(Q1, bolus)
∧ t
≤ t
+20]]
∧
[
e
= enq(Q1, empty)
→∃
!(
e
,t
)
.
[
e
= deq(Q1, empty)
∧ t
≤ t
+20]]
∧
[
e
= enq(Q1, non-empty)
→∃
(16)
!(
e
,t
)
.
[
e
= deq(Q1, non-empty)
∧
t
≤
t
+ 20]]]
.
For periodic tasks
AC
and
PM
, when a message is present in a queue, it may
be processed nearly two periods later as illustrated in Figure 3 (for
AC
).
AC
is dispatched at the beginning of each period, but can only execute in boxed
durations where the FreeRTOS schedules
AC
by switching it in and out. Sup-
pose there is a
check
function in the
AC
's implementation to check if there is
an empty message in Q3. It may happen that the
check
function is executed at
the very beginning of one period, slightly before the message empty is put to
Q3 (in which case
AC
does not know there is a message empty during the rest
of the period); in the following period, the
check
function may be executed at
the very end of the period.
This scenario is the worst case for a periodic task to detect a message in a
queue. Therefore, the constraints for
AC
and
PM
are respectively:
γ
AC
:=
∀
(
e, t
)
.
[[
e
= enq(Q3, empty)
→∃
!(
e
,t
)
.
[
e
= deq(Q3, empty)
∧ t
<t
+ 1000]]
∧
[
e
= enq(Q3, non-empty)
→∃
!(
e
,t
)
.
[
e
= deq(Q3, non-empty)
∧ t
<t
+ 1000]]]
(17)
