```Verification of Hybrid Systems
An Assessment of
Current Techniques
Holly Bowen
Verification Methods


Formal verification – determining whether given
properties are true for a given model of a
dynamic system
specification using logical proof systems


Not restricted to finite-state systems
Model checking – using the state-transition
relation in iterative computations to arrive at the
set of states for which the specification is true

Algorithmic technique
Model Checking


Requires the construction of a finite-state
approximation of the continuous dynamics
Verification of properties for the finite-state
approximation may be inconclusive!


E.g. if a state is reachable in the finite-state
approximation, that doesn’t imply it is reachable in the
underlying hybrid system
Tools can refine the approximation, but refinement will
not necessarily terminate
Example:
Batch Reactor System
Discrete
controller:
vA, vB, vC, vO
Variables:
TR, VR, tR, cA
Exothermic reaction: 2A + B  D
Operation Procedure
Formal verification: Are the forbidden states
(z5, z6) reachable?
Hybrid Model of System
Model Checking Tools
UPPAAL
 HYTECH
 d/dt
 CheckMate
 VERDICT

UPPAAL




Systems are represented as networks of timed
automata (TA)
Can analyze simple liveness properties and
reachability properties
Uses clock difference diagrams to represent TA
in a compact format
User must manually translate the process
behavior into a set of concurrent TA
UPPAAL
reactor behavior
Desired states:
S2, S5, S9
Result:
S10 is reachable!
operation procedure
HYTECH



Specifications are given as temporal logic
expressions
Uses symbolic model checking in the continuous
state space
Can only model flows with form A x  B
(linear hybrid automata)
HYTECH

Three approaches to verify systems of higher
complexity than LHA:

Clock transition models – continuous state variables
are replaced by clock variables (pure integrators with
different rates)
• Constraints identify regions for which given rates are valid


Rate translation – Retains original state variables, but
approximates continuous behavior with piecewiseconstant bounds on first derivatives
Linear phase-portrait approximation – Derivatives
of state variables can be constrained in linear
combinations
• Gives a better approximation to original state equations
Rate Translation
d/dt



Performs reachability analysis for hybrid systems
with linear continuous dynamics
Face-lifting – computing collections of orthogonal
polyhedra to represent reachable sets
Allows models with uncertainty in the input in
the dynamics equations


E.g.
x  Axlinearize
 Bu , u  U system dynamics around the
User must
operating point of interest
Face Lifting
Each face is moved by
an amount that
bounds all possible
trajectories starting on
the face
CheckMate



MATLAB-based tool, handles systems with
arbitrary nonlinear continuous dynamics
simulation
Verification:





Logical operators (AND, OR, XOR, etc.)
MUX/DEMUX
Switched Continuous System Block (SCSB)
Polyhedral Threshold Block (PTHB)
Finite State Machine Block (FSMB)
CheckMate



Computes finite-state approximation using
general polyhedral over-approximation to sets of
reachable states for continuous dynamics
Can refine current approximation and attempt
verification again if result is inconclusive
Searches for states that led to failure, splits
them, recomputes reachable states, evaluates
logic expression again
CheckMate
PHTBs
Controller
(FSMB)
CheckMate
c  0 .2
within 1 hour?
VERDICT




Modular modelling/verification of timed/hybrid
systems
Structure of system is built in a modular manner
Behavior of each module is described by a
discrete, timed, or hybrid transition system
Translates the model into the input languages of
different model checkers for discrete/timed
automata

HYTECH, KRONOS, SMV, UPPAAL
VERDICT
hybrid
behavior
controller
Comparisons

Two key issues:

Computation takes hours – only very small systems can
be verified!
• Modularity: break systems down into smaller pieces

Interpretation of results – cause of failure is not clear
Making Tools Useful for
Industry

Connecting with Existing Models


Tools for Exploring Models and Results


Model-building process is time-consuming, could
introduce errors
Useful results are obtained only when the user is
directing the verification process
Tools for Building Verification Specifications &
Interpreting Results

Difficult to translate requirement specifications into
formal specifications to be verified
```