Information Technology Reference
In-Depth Information
be performed. The
CORRECTING
phase is entered when matching correcting
modes have been identified. During this phase, maneuvers associated with the
correcting modes will cause the distance between trac agents to increase, even-
tually allowing them to reenter the
FAR
phase. For instance, TCAS distinguishes
maneuvers like “descent”, “maintain level”, and “climb” for aircrafts.
The cycle of transitions numbered (1) to (3) in the diagram thus characterizes
successful collision avoidance maneuvers. Other phases and transitions shown in
Fig. 7 increase the robustness of the protocol, by providing recovery actions in
case of failures (e.g., disturbed communication channels) in the
NEGOTIATION
phase, and can only be offered by agents with fail-safe states (like trains). For
instance, in its
RECOVERY
phase a train may initiate a braking maneuver to
avoid a collision with a preceding train.
Stipulating the pattern in Fig. 7, we proposed a generic proof rule that de-
composes the global safety proof of collision freedom (for the case of two trac
agents) into a number of simpler properties that involve only parts or limited
aspects of the agent system. The proof rules employs two key concepts: a
safety
envelope
surrounding each trac agent and a
criticality function
providing an
abstract measure of the distance between the trac agents. The rule states that
for all trac agents
A
and all criticality functions
cr
satisfying the verification
conditions VC of the rule, collision freedom is guaranteed:
A
|
= VC
⇒
A
|
=
¬
collision
where
cr
may occur in VC but not in the
collision
predicate. In an application
we have to show that the verification conditions VC are satisfied by the concrete
trac agents
A
0
and the concrete criticality function
cr
0
substituted for
cr
:
A
0
|
= VC[
cr
0
/
cr
]
Thus the proof rule, when instantiated with
A
0
and
cr
0
, yields the desired prop-
erty of collision freedom:
A
0
|
=
¬
collision
.
In Subsection 4.3 we show that criticality is a
Lyapunov-like function
and that
(for certain dynamics) the concrete function
cr
0
can be discovered automatically.
Formalization. Now we outline the formalisation of the approach as given in
[13]. A trac agent
A
is represented as the parallel composition of a plant
P
and
a controller
C
,insymbols
A
=
P
||
C
. Each of these components is modelled
,
Var
,
R
d
,
R
c
,
m
0
,Θ
) defining trajectories
by a hybrid automaton
H
=(
M
π
=(
M
,
(
X
)
X
∈
Var
)
where
M
:
Time
and
X
:
Time
→
M
→
R
for
X
∈
Var
. For details see Appendix
A and for an example see Fig. 9.
To specify behavioural properties over time of hybrid automata and state the
verification conditions of our proof rule for collision freedom, we use the State
Search WWH ::
Custom Search