Information Technology Reference
In-Depth Information
A Proof Rule for Collision Freedom. For two cooperating trac agents
A
1
=
C
1
P
1
and
A
2
=
C
2
P
2
the proof rule of [13] has the form
(VC 1)
,...,
(VC 18)
C
1
P
1
C
2
P
2
|
=
¬
collision
where the verification conditions (VC 1) ...(VC 18) require only verification
tasks of the following types:
(A) off-line analysis of the dynamics of the plant in fixed modes,
(B) mode invariants for
C
1
C
2
,
(C) real-time properties for
C
j
,
(D) local safety properties, i.e., hybrid verification tasks for
C
j
P
j
.
In the following we give a flavour of these verification conditions.
Criticality and safety.
Our approach to establishing collision freedom is to re-
duce this to an analysis of the criticality of the system. The criticality measure
separates safe from unsafe states: here a constant
c
safe
of type
R
>
0
represents the
level of criticality below which the two travel agents are
safe
, i.e., in no danger
of a collision. The following type A verification condition checks this property.
(VC 1)
Safety
Th
(
R
)
|
=
cr
<
c
safe
⇒¬
collision
This yields
P
1
P
2
|
=
cr
<
c
safe
⇒¬
collision
.
Phase-transition diagram.
It is straightforward to generate verification condi-
tions enforcing compliance of the concrete protocol to the phase-transition sys-
tem of Fig. 7. To this end, the phases
far away, negotiating, correcting, recovery
and
fail-safe
of the controllers
C
i
are represented as disjoint subsets
FAR
(
C
i
),
NEG
(
C
i
),
COR
(
C
i
),
REC
(
C
i
),
FSA
(
C
i
)
⊆
M
i
of the set of modes. When spec-
ifying the behaviour of the controllers
C
i
in DC, we use
FAR
(
C
i
) as a shorthand
for
M
(
C
i
)
FAR
(
C
i
) and analogously for the other phases. Then we check the
following simple type B verification condition.
∈
(VC 2)
Controllers observe phase-transition diagram. For
i
=1
,
2
C
i
|
=
0
Φ
phase
(
C
i
)
Thus the controllers satisfy the above phase constraints from the start. Here
Φ
phase
(
C
i
) is a conjunction of formulae of the following type:
Initial phase
:
∨
FAR
(
C
i
)
; true
for
i
=1
,
2
Phase sequencing
:
FAR
(
C
i
)
−→
FAR
(
C
i
)
∨
NEG
(
C
i
)
for
i
=1
,
2
..................etc ...............
Search WWH ::
Custom Search