Information Technology Reference
In-Depth Information
Adequacy.
The following type A verification condition ensures that the critical-
ity does not increase when collision avoidance maneuvers are activated. Note
that these are part of the hybrid automata resulting from the restriction of the
controller to the selected correcting mode.
(VC 15)
Adequacy of matching modes. For all (
m
1
,
m
2
)
∈
MATCH
C
1
m
1
P
1
C
2
m
2
P
2
|
=
↑
Φ
(
m
1
,
m
2
); true
⇒∀
c
∈
R
≤
0
:
cr
≤
c
−→
cr
≤
c
For the recovery maneuver, a similar verification conditions additionally requires
that after a suitable braking time
t
depending on their speeds at the start of the
maneuver, the trac agents have come to a complete halt.
Far away phase.
The following type B verification conditions enforces that the
correcting phase can be left in favour of the phase
far away
only when there is
no warning that new correcting maneuvers have to start in
Δ
C
time.
(VC 17)
Termination of maneuvers. For
i
=1
,
2 and
φ
F
⇔¬
φ
N
↑Φ
F
−−−→
C
i
P
1
P
2
|
=
COR
(
C
i
)
FAR
(
C
i
)
Fail-safe state.
The following type B verification condition ensures that the
recovery maneuver is concluded by entering the fail-safe state, when the agent
has come to a complete stop. By (VC 2), each trac agent stays in this state.
We require that in this state the trac agent does not change its position, and
that the criticality does not increase.
(VC 18)
Fail-safe state. For
i
=1
,
2
↑
(
spd
i
=0)
−−−−−−→
C
i
P
i
|
=
REC
(
C
i
)
FSA
(
C
i
)
∧
spd
i
=0
C
i
P
1
P
2
|
=
∀
c
∈
R
≥
0
:
FSA
(
C
i
)
∧
spd
i
=0
∧
cr
≤
c
−→
spd
i
=0
∧
cr
≤
c
.
In [13] the following was shown.
Theorem 1 (Soundness).
The verification conditions
(VC 1),...,(VC 18)
together imply
C
1
P
1
C
2
P
2
|
=
¬
collision
,
i.e., the proof rule for collision freedom is sound.
4.2
Case Study: Movement Authority
Let us revisit the ETCS train control introduced in Subsection 2.4. However, in-
stead of using Matlab-Simulink and Stateflow as modelling techniques, we shall
now represent the scenario more abstractly by time-dependent observables and
Search WWH ::
Custom Search