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

increases the computational cost for proving safety properties (see Section 7).
For linear/ane dynamics, the discretized system can then be computed through
the matrix exponential e A τ ,where τ is the sampling rate and A the matrix
representing the dynamics (i.e., x • = Ax ).
For such a discrete-time hybrid system with dynamics given as difference
equations, asymptotic stability can be shown using the same methods as for the
continuous case [16]. Again a (slightly different) set of LMIs can be obtained
and solved through convex optimization. For instance, for a sampling rate of 0 . 1
seconds, the following Lyapunov function was obtained:

s 2 +0 . 0172 v 0 ) 2

V ( v − v 0 , s )=0 . 0105 ∗ ∗ ( v − v 0 ) ∗ s +6 . 0591 ∗ ( v −

6.5 Stability of the Sampled-Data Drive Train

Stability analysis of discrete-time hybrid systems can also be used to shed light
on stability properties of sampled-data systems, that is control loops with con-
tinuous plant and discrete controller. In this case sensor measurements are sent
to the controller in periodic intervals. The actuators will also periodically receive
updates from the controller.
In case of linear plant dynamics, stability analysis can be conducted on a
purely discrete-time system which is obtained by also discretizing the plant via
zero-order-hold discretization. This procedure is lossless in case of a non-hybrid
linear plant because the state of the plant at each sampling instant can be
exactly computed from its state at the previous sampling instant and the current
controller output. If the plant is hybrid, but with linear dynamics, the dynamics
can still be discretized exactly, but the switches are possibly inexact. With the
absence of so-called “grazing switches” [15], it is usually possible to approximate
the sampled system closely enough.
For the drive train system, we have performed this kind of analysis for a fixed
sampling rate (0 . 1 seconds) and a discrete controller obtained by a textbook dis-
cretization method for linear systems (zero-pole matching transformation [17]).
The resulting sampled-data system consists of the continuous-time drive train
dynamics given in Subsection 2.1 and the discretized controller, and it can still
be proven stable by this method.

7 Proving Safety of Local Control and Design Models

In this section, we present our approach of model checking safety properties of
local control and design models of the example. We first outline our general
methods for verification of hybrid systems with non-trivial discrete behaviour
(Subsections 7.1 and 7.3); then we build both continuous-time and discrete-time
models of the system based on its Matlab-Simulink description and show model
checking results of these models (Subsections 7.2 and 7.4).