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

an early request because other trac agents occupy the track segment beyond
EoA.
Constraints on the parameter ST can be derived [45] from an analysis of a
single negotiation and correction phase. A proof yields the following necessary
constraint depending on the expected maximum RBC communication latency L :

Lv + v 2
2 b

ST ≥ . (20)

Again, (20) corresponds to a version of (13) that has been synthesized from the
system model deductively.
The constraints (19) and (20) can be used to find out how dense a track can
be packed with trains in order to maximize throughput without endangering
safety, and how early a train needs to start negotiation in order to minimize the
risk of having to reduce speed when the MA is not extendable in time.

6 Proving Stability of Local Control and Design Models

Stability is a property of a dynamic system that subsumes its ability to with-
stand, and eventually compensate for, outside disturbances that affect a system.
For a local closed-loop control system, this is a very desirable property, be-
cause stability ensures that the controller is actually able to keep the controlled
parameter close to the desired value. Furthermore, if one requires asymptotic
stability, there cannot be any undamped oscillations or cyclic behavior in the
closed-loop system. For instance, one would expect from a speed controller for
a train, that it forces the speed to converge toward a desired value, without
producing needless cycles of acceleration and deceleration. Very little controller
activity should be needed, once the train is close to this desired speed. In this
section, we will apply methods based on the concept of Lyapunov-functions [35]
to the speed controller of the train model from Section 2. Lyapunov functions
are functions that map each system state onto a nonnegative real value. For
every run of the system, the sequence of values this function attains is required
to be decreasing, eventually converging to zero at the desired control point. If a
function with these properties is found, then the system is asymptotically stable .
We will detail how methods for automatic computation of these functions can
be applied to a model of a speed controller.

Definition 4. Consider a continuous-time dynamic system with state vector
x

n .Letx ( t ) ,t

0 , denote its state at time t during a run of the system.
The system is called globally asymptotically stable if the following two properties
hold for all possible runs:

∈ R ≥

a) ∀ > 0 ∃ δ> 0 ∀ t ≥ 0: || x (0) || <δ ⇒|| x ( t ) || < (stability)

b) t →∞⇒ x ( t ) → 0 (global attractivity)

If a) and b) hold only on a bounded set containing 0 , the system is called locally
asymptotically stable .