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

Step computation. Our model checker can handle continuous-time models, which
contains both discrete transitions and continuous flows. Discrete transitions are
given in the form of guarded assignments , while continuous flows are given in the
form of modes , which define the evolution of continuous variables by constants.
For each mode there is a boundary condition, the mode is left as soon as the
boundary condition is satisfied.
For checking an invariance property, the model checker performs a symbolic
backward reachability analysis, to ensure that no state in the complement of the
property is reachable from the initial state set. The key achievement lies in the
capability of reducing this backward analysis to pure substitution. It can be done
easily for discrete transitions as detailed in [12]. The capability of representing
as well the effect of continuous flows through substitution rests on our ability
to perform pre-image computations for arbitrary Boolean combinations of linear
constraints using the Loos-Weispfenning quantifier elimination method [34]. In
contrast to other verification methods for hybrid systems, this allows us to handle
non-convex polyhedra directly [11]. Note that during each step computation new
linear constraints can be introduced, thus the set Q is dynamically updated.

Example 1 (Discrete transitions). Assume that we want to check an invariance
property

FAIL , stating that the failure state can never be reached. In the
model, one discrete transition can set the Boolean variable FAIL to true:

¬

REC ∧ ( v ≤ 0 . 0) ∧ ( p > EoA ) → FAIL := true ;

The transition says that if currently the cooperation protocol is in the REC
phase, the train has come to a stop, and the position of the train is beyond
the end of authority point (EoA), then the system reports a failure. One back-
ward step computation of such transition leads to the following state-set (after
optimizations in Lin-AIGs):

¬ FAIL ∧¬ ( REC ∧ v ≤ 0 . 0 ∧¬ ( p < = EoA )).

Example 2 (Continuous flows). The pre-image of the state-set in the previous
example under the mode with continuous evolution v • =0 . 0

p • = v d

∧ and

boundary condition p < EoA − ST (start talking) will remain the same.

Fix-point detection. We need to perform subsumption checks to detect whether
a fixpoint has been reached during model checking. In our approach, since linear
constraints enter the state-set descriptions, one has to check implications between
two state-set representations. We use HySAT [18] for this purpose.

Optimizations. Using ecient methods for keeping the state-set representation
as compact as possible is the key point for our approach. This is achieved by
integration of different techniques, ranging from purely Boolean methods to (in-
creasingly) exploiting knowledge about linear constraints.

- We use inexpensive methods such as simulation, test-vector generation, de-
tection of implications between linear constraints, and propagation of learned
implications to simulation vectors to identify inequivalent Lin-AIG nodes.