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

the computation. Condition (VC 15) is implied by the Lyapunov-like condition
V • ( x ) 0 stating that V cannot increase over time.

Therefore, a criticality function as needed in (VC 1), (VC 5) and (VC 15)
can be computed automatically, using methods for Lyapunov function synthesis.
The dynamics for the given tuple of maneuvers is needed as an input, as is
the set of unsafe states. Condition (VC 4) needs to be checked separately,
since a Lyapunov-like function does not guarantee that the set

≤

}
is always entered before a trajectory can pass into the unsafe region U .Itis
then possible to synthesize a Lyapunov-like boundary function (serving as the
criticality function) and a contour line value k (serving as the maximal admissible
criticality level) such that initiating the maneuver with criticality lower than k
guarantees safety. Each admissible set of initial state vectors S for the maneuver
corresponds to a possible safe condition for the maneuvers.
For the rail-road crossing case study, will now employ Lyapunov-like boundary
functions to identify a safe guard Φ , such that pos

{ x | V ( x ) < k

≤ EoA is always guaranteed.

Therefore we put U = .As Φ is not given, but to be derived, we

define Φ := V ( x ) < k . All states with this property are separated from U by
the contour line V ( x )= k .
Since a system can potentially have many admissible criticality functions,
this even holds for any state within a contour line of any criticality function
withrespecttothesameunsaferegion U . Therefore, we are not restricted to
one function, but can use many. The predicate Φ is then the disjunction of the
predicates V i ( x ) < k for all such criticality functions V i and associated contour
line values k i . Using many criticality functions instead of one can result in a
weaker, and therefore less conservative, predicate Φ .
For the case study, it was sucient to use just one criticality function, as
the use of several functions brought no significant improvement. As a result we
obtained the following criticality function cr and boundary value c safe :

{ pos > EoA }

EoA + 2000) 2 + spd 2

cr =0 . 0014616 ∗ ( pos − (15)

c safe = 5846 . 445 (16)

Figure 12 shows the position of the train in meters before the EoA point
on the horizontal axis and its velocity in m / s on the vertical axis. The shaded
set of states is safe set { x | V i ( x ) < k i } . Initiating the braking within this
set guarantees that the unsafe region to the right of the vertical line cannot be
entered. For this particular example, where the speed is decreasing at a fixed rate,
this implies an eventual transition to the FailSafe phase, without breaching any
safety requirements. Furthermore, assuming a maximal speed v max =76 . 46 m / s ,
condition (VC 4) is also fulfilled, since system trajectories could not enter the
unsafe region without first passing through the ellipsoid. Any predicate Φ which
evaluates to false everywhere outside this set is admissible as a guard for the
transition between the Appr and Braking modes.