IA169 System Verification and Assurance
Verification of Real-Time and Hybrid systems
Jiří Barnat
Verification in Model-Based Development
Software Engineering Experience
Employing V&V techniques too late in the development
process significantly increases the cost of poor quality.
The sooner a bug is detected the cheaper is the fix.
Model-Based Development
Model-Based Verification
Model-Based Development
Consider models of the target system in order to ,e.g.,
simulate its behaviour in the design phase prior
implementation.
Behavioural models can be used for verification.
IA169 System Verification and Assurance – 11 str. 2/48
Hybrid Systems
Hybrid Systems
Systems that combine multiple kinds of dynamics.
Continuous systems driven by discrete events.
Areas of existence
Mechanical systems
Continuous movement and contact with physical obstacle.
Electrical systems
Continuous nature of electric charge in circuit driven by
discrete switches.
Embedded systems
Computer-driven systems in analogue environment.
IA169 System Verification and Assurance – 11 str. 3/48
Example – Bouncing Ball
System Description
A ball released at height h bounces on a hard surface. The
ball is under continuous influence of the gravity (9.8m/s).
When bounces some energy is consumed by friction and
elasticity and turns into heat.
Physics
Acceleration = First derivative of speed with respect to time.
Speed = First derivative of height with respect to time.
Abstraction and simplification
Modelled with a mass point.
Instant (time-less) bounce.
IA169 System Verification and Assurance – 11 str. 4/48
Bouncing Mass Point – Hybrid Automaton
Automaton Description
x1 — height
x2 — vertical speed (+ means up, − means down)
c ∈ [0, 1] — loss of energy (elasticity and heat)
Schema
IA169 System Verification and Assurance – 11 str. 5/48
Analyses and Control of Hybrid Systems
Questions
What time elapses between the fourth and fifth bounce?
If given horizontal speed, will the ball jump over an obstacle?
. . .
Searching for Answers
Need for precise formal description of hybrid system.
Algorithmic analysis of properties of hybrid systems and
controller synthesis.
IA169 System Verification and Assurance – 11 str. 6/48
Section
Hybrid Automata
IA169 System Verification and Assurance – 11 str. 7/48
Hybrid Automata
Hybrid Automaton is a tuple
Q = {q1, q2, . . .} — Set of discrete states.
X = Rn — Set of continuous states.
f : Q × X → Rn — System dynamics.
Init ⊆ Q × X — Set of initial states.
Dom : Q → PowerSet(X) — State invariants.
E ⊆ Q × Q — Set of discrete transitions
G : E → PowerSet(X) — Map of transition guards.
R : E × X → PowerSet(X) — Map of transition resets.
IA169 System Verification and Assurance – 11 str. 8/48
State of Hybrid Automaton
State of Hybrid Automaton
Given by the discrete state and the current value of
continuous variables: (q, −→x ) ∈ Q × X.
Initial State
Set of initial states in both the discrete and continuous part.
(q0, −→x0 ) ∈ I
IA169 System Verification and Assurance – 11 str. 9/48
Transitions of Hybrid Automaton
Transition by Time Passing
Let (q, −→x ) be origin state.
Continuous part for every variable x follows the system
dynamics
dx(t)
dt
= f (q, x), where x(0) = x
Discrete part does not change:
q(t) = q
Time may pass only if the state invariant is valid:
x(t) ∈ Dom(q)
IA169 System Verification and Assurance – 11 str. 10/48
Transitions of Hybrid Automaton
Discrete Transition
Let (q, −→x ) be origin state.
It is possible (but not necessary) to perform a transition
(q, q ) ∈ E,
if transition guard is valid, i.e.
−→x ∈ G(q, q ).
If the transition is taken, the continuous part of the state is
updated accordingly:
−→
x := R((q, q ), −→x )
The target state after a discrete transition is (q ,
−→
x ).
IA169 System Verification and Assurance – 11 str. 11/48
Reasonable restrictions of Hybrid Automata
Restrictions in Continuous Part
f (q, −→x ) is Lipschitz continuous for ∀q ∈ Q,
(solution of differential equations is well defined)
∀e ∈ E we assume non-empty G(e)
∀e ∈ E and ∀x ∈ Q we assume non-empty R(e, x)
Restrictions in Discrete Part
The set of discrete state is finite.
IA169 System Verification and Assurance – 11 str. 12/48
Example 2 – Water Tank
System Description
Two water tanks, volume of water denoted with x1 and x2.
There is a constant speed leak from both tanks, v1 and v2.
A hose can fill one of the tanks with speed w.
The hose is always in exactly one of the tanks.
IA169 System Verification and Assurance – 11 str. 13/48
Example 2 – Water Tank
Goal
Keep water level above the necessary minimum r1 and r2.
Initially, there is enough water in both tanks.
The hose is switched to a tank at the moment the water level
in the tank drops to the required minimum.
IA169 System Verification and Assurance – 11 str. 13/48
Water Tanks — Formal Definition of the System
Q = {q1, q2}
X = R × R
f (q1, x) =
w − v1
−v2
f (q2, x) =
−v1
w − v2
IA169 System Verification and Assurance – 11 str. 14/48
Water Tanks — Formal Definition of the System
Init = {q1, q2} × {x ∈ R × R | x1 ≥ r1 ∧ x2 ≥ r2}
Dom(q1) = {x ∈ R × R | x2 ≥ r2}
Dom(q2) = {x ∈ R × R | x1 ≥ r1}
IA169 System Verification and Assurance – 11 str. 14/48
Water Tanks — Formal Definition of the System
E = {(q1, q2), (q2, q1)}
G(q1, q2) = {x ∈ R × R | x2 ≤ r2}
G(q2, q1) = {x ∈ R × R | x1 ≤ r1}
R(q1, q2, x) = R(q2, q1, x) = {x}
IA169 System Verification and Assurance – 11 str. 14/48
Hybrid Time Sequence (HTS)
Informally
A run of hybrid automaton proceeds in a sequence of
continuous time intervals. Discrete transitions happen on the
boundaries of the intervals in instant time.
The time characteristic of a run of hybrid automaton is
formalised with the usage of the so called Hybrid Time
Sequence.
Definitions
Hybrid Time Sequence is a (finite or infinite) sequence of
intervals τ = {I0, I1, . . . , IN} = {Ii }N
i=0 such that:
Ii = [τi , τi ] for all i < N
If N < ∞ then either IN = [τN, τN] or IN = [τN, τN)
τi ≤ τi = τi+1 for all 0 ≤ i < N.
IA169 System Verification and Assurance – 11 str. 15/48
Graphical Representation of Hybrid Time Sequence
IA169 System Verification and Assurance – 11 str. 16/48
Ordering of Time Moments
Observation
If every time moment is related with an interval of HTS ...
... then time moments can be linearly ordered.
Ordering
t1 ∈ Ii , t2 ∈ Ij
t1 t2
def
= (t1 < t2) ∨ (t1 = t2 ∧ i < j)
Generalisation
Every hybrid time sequence is linearly ordered with relation.
IA169 System Verification and Assurance – 11 str. 17/48
Ordering of Hybrid Time Sequence
Prefix Of Hybrid Time Sequence
τ = {Ii }N
i=0
ˆτ = {ˆIi }M
i=0
We say that τ is a prefix of ˆτ (denoted with τ ˆτ), if
τ = ˆτ, or
N is finite ∧ IN ⊆ ˆIN ∧ ∀i ∈ [0, N) : Ii = ˆIi
Proper Prefix
τ ˆτ ≡ τ ˆτ ∧ τ = ˆτ
Relation is a Partial Ordering
There exist τ and τ such that τ τ and τ τ.
IA169 System Verification and Assurance – 11 str. 18/48
Task
Task – Find τ, τ and τ such that
τ τ
τ τ
τ τ ∧ τ τ
Solution
IA169 System Verification and Assurance – 11 str. 19/48
Hybrid Trajectories
Definition
Hybrid trajectory is a triple (τ, q, x), where τ is hybrid time
sequence τ = {I}N
0 and q, x are two sequences of functions
q = {qi }N
0 and x = {xi }N
0 such that qi : Ii → Q and
xi : Ii → Rn, respectively.
Intuition
Continuous part flows within individual time intervals of
hybrid time sequence.
Discrete state within a single interval does not change.
Discrete transitions realise transitions from the end of one
interval to the beginning of the succeeding interval.
IA169 System Verification and Assurance – 11 str. 20/48
Run of Hybrid Automaton
Run of Hybrid Automaton
Let H = (Q, X, f , Init, Dom, E, G, R) be hybrid automaton.
Let (τ, q, x) be hybrid trajectory.
Trajectory (τ, q, x) is a run of automaton H, if it is compliant
with H in: initial condition, discrete behaviour and continuous
behaviour.
Initial Condition
(q0(0), x0(0)) ∈ Init
Discrete Behaviour – For all i < N it holds that
(qi (τi ), qi+1(τi+1)) ∈ E
xi (τ ) ∈ G(qi (τi ), qi+1(τi+1))
xi+1(τi+1) ∈ R(qi (τi ), qi+1(τi+1), xi (τi ))
IA169 System Verification and Assurance – 11 str. 21/48
Run of Hybrid Automaton
Run of Hybrid Automaton
Let H = (Q, X, f , Init, Dom, E, G, R) be hybrid automaton.
Let (τ, q, x) be hybrid trajectory.
Trajectory (τ, q, x) is a run of automaton H, if it is compliant
with H in: initial condition, discrete behaviour and continuous
behaviour.
Continuous Behaviour – For all i ≤ N it holds that
qi : Ii → Q is constant over t ∈ Ii ,
xi : Ii → X is a solution to differential equation
dxi (t)
dt
= f (qi (t), xi (t))
over Ii beginning in xi (τi ),
For all t ∈ [τi , τi ) it holds that xi (t) ∈ Dom(qi (t)).
IA169 System Verification and Assurance – 11 str. 21/48
Water Tanks – Example
Specification
τ = {[0, 2], [2, 3], [3, 3.5]}
Constants r1 = r2 = 0, v1 = v2 = 0.5, w = 0.75
Initial state q = q1, x1 = 0, x2 = 1.
IA169 System Verification and Assurance – 11 str. 22/48
Water Tanks – Trajectories
IA169 System Verification and Assurance – 11 str. 23/48
Classification of Runs (τ, q, x)
Finite
If τ is finite and the last interval of τ is closed.
Infinite
If τ is infinite sequence, or the sum of time intervals in τ is
infinite, i.e.
ΣN
i=0(τi − τi ) = ∞.
Zeno
If τ is infinite, but
ΣN
i=0(τi − τi ) < ∞.
Maximal
If τ is no proper suffix of any other run τ of H.
IA169 System Verification and Assurance – 11 str. 24/48
Classification of Runs
τA finite; τC and τD infinite; τE and τF Zeno.
What class is run τB?
IA169 System Verification and Assurance – 11 str. 25/48
Examples of ZENO Runs
IA169 System Verification and Assurance – 11 str. 26/48
Examples of ZENO Runs
Let
Then
the following hybrid system has infinitely many intersections
with x axis in the interval (− , 0].
IA169 System Verification and Assurance – 11 str. 27/48
Modelling Hybrid Systems
Observation
Hybrid automata are meant to describe real hybrid systems.
Due to abstraction and simplification, it is possible to specify
unrealistic situation.
Risk of Modelling
Can create system that have no solutions.
Can create system that have only unrealistic solutions.
Can create system that have non-deterministic solutions.
Terminology
System that has no solution (no run exist) is called blocking
system.
IA169 System Verification and Assurance – 11 str. 28/48
Unrealistic Runs
Observation
Non-blocking system does not guarantee that some runs are
realistic.
Non-blocking system does not guarantee that some runs are
time divergent.
Unrealistic Runs
Runs that perform infinitely many discrete transitions in finite
time are called ZENO runs.
Created by abstraction and simplification in modelling.
Discussion
Why the ball does not bounce forever?
It is important to see which simplification lead to ZENO runs.
IA169 System Verification and Assurance – 11 str. 29/48
Non-determinism
Non-determinism
In general can be described as absence of unique solutions, i.e.
that a hybrid automaton accepts multiple different runs
emanating from the same initial conditions.
When limited to Lipschitz continuous functions with unique
solution, reason for non-determinism comes from discrete
transitions.
Non-deterministic on Purpose
Can be used to model uncertainty.
Modeller should make difference between non-determinism
due to simplification, and non-determinism used on purpose.
Observation
Non-determinism is a real cause of troubles in both analysis
and controller synthesis of hybrid systems.
IA169 System Verification and Assurance – 11 str. 30/48
Problems of Simulations and Analysis of Hybrid Systems
Existence of Solution
How to detect existence of non-blocking run?
How to detect ZENO behaviour?
Uniqueness
How to perform simulation of non-deterministic system?
Discrete transition vs. continuous time evolution.
Discrete transition vs. discrete transition.
As-soon-as semantics.
Discontinuity
How to detect satisfiability of transition guards?
What if state invariant ends with open interval [a, b) and the
succeeding transition is allowed to execute at time [b]?
Composition
How to compose hybrid automata?
IA169 System Verification and Assurance – 11 str. 31/48
Non-blocking and Deterministic Hybrid Automaton
Non-blocking Hybrid Automaton
Hybrid automaton H is called non-blocking if for all initial
states (ˆq, ˆx) ∈ Init there exist an infinite run emanating
from (ˆq, ˆx).
Deterministic Hybrid Automaton
Hybrid automaton H is called deterministic, if for all initial
states (ˆq, ˆx) ∈ Init there exist at most one maximal run
emanating from (ˆq, ˆx).
IA169 System Verification and Assurance – 11 str. 32/48
Section
Using Hybrid Automata
IA169 System Verification and Assurance – 11 str. 33/48
Analysis and Synthesis Hybrid Systems (HS)
Motivation for Modelling
The goal of modelling of HS is to deduce properties of, or
synthesise controllers for real HS from properties of, or
controllers for modelled HS.
Verification
Does hybrid system exhibits declared behaviour (does it
satisfy specification)?
Synthesis
There are number of choices to build a HS, using models it is
possible to decide which choices are good and which are bad
prior the construction of the real HS.
IA169 System Verification and Assurance – 11 str. 34/48
Validation
Validation
Check that the design described as a hybrid automaton and
the real product produced behave accordingly.
Some system modelled with hybrid automata may be
unrealistic (and cannot be built) due to simplifications and
abstractions used during modelling phase.
Usual Work-flow
Synthesis (of model)
Verification (of model)
Validation (equivalence of model and real product)
IA169 System Verification and Assurance – 11 str. 35/48
Specification
Stability
Typical property of purely continuous systems.
To request stability for hybrid systems requires to specify what
does the stability means with respect to the discrete part of
the system.
Specification by Set of States
Specification of safety and forbidden areas.
Specification by Set of Trajectories
Properties of hybrid systems that can be expressed as
properties of runs.
Set of allowed runs of a hybrid automaton.
Formally described using modal and temporal logic, such as
(CTL, LTL, CTL∗).
IA169 System Verification and Assurance – 11 str. 36/48
Methods of Analysis of HS
Deductive Methods
Using math reasoning, such as math induction, to deduce
properties of hybrid systems.
Can be automated.
Model Checking
Algorithmic procedure for deciding formally specified
properties of hybrid systems.
Decidable only for limited sub-classes of hybrid automata.
Simulations
Used to estimate the set of reachable states.
The precision of estimation is difficult to say.
IA169 System Verification and Assurance – 11 str. 37/48
Deductive Methods – Invariant Set
Typical Goal
Typical goal for deductive methods is to set boundaries of the
reach set using the so called Invariant Set.
Invariant set is a set of states for which it holds that if a run
of hybrid system is initiated at the state of the set it only
visits states that are in the set (i.e. never leaves invariant set).
Formal Definition of Invariant Set
Set of state M ⊆ Q × X of hybrid automaton H is called
invariant if for all (ˆq, ˆx) ∈ M, all solutions (τ, q, x) starting
from (ˆq, ˆx), all Ii ∈ τ and all t ∈ Ii it holds that
(qi (t), xi (t)) ∈ M.
IA169 System Verification and Assurance – 11 str. 38/48
Deductive Methods – Properties of Invariant Set
Observation
Union and Intersection of Invariant Sets of hybrid automaton
H is also an invariant set for H.
If M is an invariant set and Init ⊆ M, then Reach ⊆ M.
Consequence
To approximate the Reach set it is possible to deduce a
number of invariant sets that contain initial state and are at
the same time below the set of all states of hybrid automaton
(here denoted by F)
Init ⊆ M ⊆ F
and intersect them.
IA169 System Verification and Assurance – 11 str. 39/48
Model Checking
Simplification
For hybrid automata we restrict ourselves in the course to
algorithmic test of reachability of a given state.
Considered Sub-classes of Hybrid Automata
Timed Automata (TA).
Rectangular Hybrid Automata (RHA).
Linear Hybrid Automata (LHA).
Software Tools
UPPAAL – Timed Automata
PHaVer – RHA, partially LHA (HyTech)
IA169 System Verification and Assurance – 11 str. 40/48
Timed Automata
Restriction
All derivations to drive continuous evolution of the automaton
has the form of:
dxi (t)
dt
= 1
Resets R of discrete transitions are allowed either to keep the
value of the continuous variable, or to reset it to 0.
Dom and G are defined only using relations ≤ and ≥ with
respect to integral values.
Intuition
Finite automaton with a set of continuous
variables to measure elapsed time.
Measured time values may be reset to 0
using discrete transition.
IA169 System Verification and Assurance – 11 str. 41/48
Example of Timed Automaton
Example of Timed Automaton
Exercise
In two-dimensional graph with axes x1 and x2 show how the
values of continuous variables change.
IA169 System Verification and Assurance – 11 str. 42/48
Region Abstraction
Key Observation
With respect to the restriction that comparisons are made
only against integral values, two floating point values that
have the same integral part cannot be differentiated.
Equivalence Classes on the Continuous Domain
If c is the greatest integral number used in a guard of timed
automaton then the continuous domain can be represented
with a finite set of intervals as follows:
[0], (0, 1), [1], (1, 2), [2], . . . [c − 1], (c − 1, c), [c], (c, ∞)
Abstracted domain is finite for every continuous variable.
It is possible to construct finite-state automaton that
faithfully simulates behaviour of the timed automaton.
This can be used for verification purposes.
IA169 System Verification and Assurance – 11 str. 43/48
Region Abstraction
IA169 System Verification and Assurance – 11 str. 44/48
Rectangular Hybrid Automata (RHA)
Restriction
All derivations to drive continuous evolution of the automaton
has the form of:
a ≤
dxi (t)
dt
≤ b,
where a and b are rational constants.
When specifying RHA no derivation equations are given, just
the boundary constants a and b.
Exercise
Consider a RHA with two continuous variables x1 and x2.
On two-dimensional graph with axes x1 and x2 show the
evolution of values of the continuous variables.
Guess the origin of the name of this particular sub-class of
hybrid automata.
IA169 System Verification and Assurance – 11 str. 45/48
Reachability is Decidable for RHA
Reachability
Reachability problem for RHA is decidable if there are only
finitely many values to which a continuous variable may be
reset by a discrete transition.
The most general sub-class of hybrid automata for which
reachability is still decidable.
Going Beyond Means Undecidability
Relaxation from restriction of resets is known to result in
sub-class of hybrid automata for which the reachability
problem is undecidable.
IA169 System Verification and Assurance – 11 str. 46/48
Linear Hybrid Automata (LHA)
Definition
Let k0, . . . , km be numeric constants and x1, . . . , xm variables.
An expression in the form of k0 + k1x1 + k2x2 + · · · + kmxm is
called a linear expression.
Let t1, t2 be linear expressions. An expression of the form
t1 ≤ t2 is called linear inequality.
Hybrid automaton H is called linear hybrid automaton
(LHA), if Init, Dom, G and f are defined as Boolean
combinations of linear inequalities.
Undecidability
The reachability problem for LHA is undecidable.
Algorithms implemented for the LHA sub-class are incomplete
(HyTech).
IA169 System Verification and Assurance – 11 str. 47/48
Practicals and Homework
Practicals
Modelling with timed automata.
UPPAAL model checker.
Follow the UPPAAL tutorial
(http://www.it.uu.se/research/group/darts/papers/
texts/new-tutorial.pdf)
Homework
Will Lake Mead go dry? (SPACEex tool).
http://spaceex.imag.fr/documentation/tutorials
IA169 System Verification and Assurance – 11 str. 48/48