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

The dynamics of this simplified RBC controller is described by the automaton
in Fig. 10. The expression update ( EoA ) abbreviates an assignment of a new,
larger value to the variable EoA .Theclock x with upper bound ε in mode
Check models the maximum delay it takes for the RBC to answer the request
for extending the EoA .

extEoA / OK := ff, x := 0

Check
x

true / OK := ff

Idle

￿

= 1

￿
￿
￿
￿

EoA

￿

= 0

EoA = 0

true / OK := tt, update(EoA) x < ε

true / OK := ff

Unsafe

Fig. 10. RBC controller

4.3 Automatic Discovery of the Criticality Functions
It is critical for a system according to Fig. 7 that a recovery maneuver will always
lead into a fail-safe state without violating any safety constraints. To ensure this,
recovery needs to be initiated in time, so that potentially hazardous situations
can be avoided. For the train example given in the previous sections, we will now
demonstrate how to determine states which lead to a safe recovery maneuver.
In this particular case we will ensure that the train will always come to a stop
before an end-of-authority point associated with a critical section. In particular,
we will construct a predicate Φ guaranteeing that the train system is safe in the
sense that no critical section can be passed, unless the RBC sent the signal OK
to the train passing it. In other words, once the train system enters the Braking
mode, the safety condition pos EoA will not be violated and the train will

come to a stop in the FailSafe mode — braking is always initiated in time.
We will now show that the criticality function in the verification conditions
from Subsection 4.1 can be seen of an instance from a generic class Lyapunov-
like functions. Methods for synthesis of Lyapunov functions can then be adapted
to automatically compute a suitable criticality function. Since contour lines of
the function can be used to separate reachable and non-reachable states, we call
this class Lyapunov-like boundary functions .
Definition 3. Let x ( t )

≤

n be a hybrid system's state vector (the vector of
the valuations of all variables 6 ) at time t. Given a set of initial states vectors

∈ R

6 For the ease of mathematical treatment, the state of the system is represented as a
vector of real numbers, instead of a function σ : Var → R like in Subsection 4.1.