Automating Verification of Cooperation, Control, and Design in Traffic Applications - Formal Methods and Hybrid Real-Time Systems - page 156

- We use HySAT [18] for reducing the size of the Lin-AIG representation by
detecting equivalent Lin-AIG nodes, which is applied only to candidates
obtained by inexpensive methods.
- We extract “don't cares” from conflicts of calls of HySAT to remove re-
dundant linear constraints in the state set representations. This allows us
to restructure Lin-AIGs based on internal node equivalences modulo “don't
cares”, and to achieve new compact representation as a Boolean combination
of a minimal subset of the original set of linear constraints.

We have demonstrated [12,11] that the tuned combination of these deeply inte-
grated methods leading to significant performance improvements.

7.2 Continuous-Time Models and Verification Results

The models of the system mainly consists of two parts: (1) a cooperation protocol
between the train and the rail-road crossing for collision avoidance, (2) a speed
supervision of the train. Compared to its original description in Matlab-Simulink,
we have made some simplifications.

The cooperation protocol. The protocol distinguishes a number of phases as
shown in Fig. 7. Additionally, we add one more transition from the RECOVERY
phase: If the train stops in front of the crossing, and the position of the train is
beyond the end of authority point (EoA), then a FAILURE phase is entered. The
safety property of collision freedom is equivalent to prove that this FAILURE
phase of the cooperation protocol can never be entered.

The speed supervision. Figure 6 gives an overview of the train speed control.
Here, we summarize the modes and the switching conditions between them in
our models, as derived from Fig. 6. For each segment of the track, there is a
pre-defined desired train speed. The modes for driving the train are decided by
the relation of the desired speed v d and the current speed v .Inthe NormalMove
mode ( v < v d ≤ 1 . 05 · v ), the train is driven under a PI controller. Once the

condition 1 . 05 v d holds, the train switches to the mode MotorOff ,

where the drive force for the train becomes zero, and the train decelerates on
a constant

· v d < v ≤ 1 . 1 ·

0 . 05 m / s 2 .Fromthe MotorOff mode, the train can re-enter the
NormalMove mode as soon as v

−

v d . If the difference between v d and v is large,
the mode EmergencyBraking ( ServiceBraking ) will be entered if v

≤

≥ 1 . 5 · v d ,( v ≥

1 . 1 v d )fromthe NormalMove mode. In modes EmergencyBraking

and ServiceBraking , the train decelerates on constants

· v d ∧ v ≤ 1 . 5 ·

1 . 0 m / s 2 ,
respectively. During ServiceBraking , the mode NormalMove ( MotorOff )isre-
entered if v

3 . 0 m / s 2 and − −

v d ). There is one special case when the
train enters the EmergencyBraking mode. Since the train is desired to stop, it
is not possible to re-enter the modes NormalMove and MotorOff . Constants in
the conditions are derived from the Matlab-Simulink model.

≤ v d (1 . 05 · v d < v ≤ 1 . 1 ·