IA169 System Verification and Assurance
LTL Model Checking
Jiří Barnat
Motivation
Checking Quality
Testing is incomplete, gives no guarantees of correctness.
Deductive verification is expensive.
Typical reasons for system failure after deployment
Interaction with environment (unexpected input values).
Interaction with other system components.
Parallelism (difficult to test).
Model Checking
Automated verification process for ...
... parallel and distributed systems.
IA169 System Verification and Assurance – 05 str. 2/36
Section
Verification of Parallel and Reactive Programs
IA169 System Verification and Assurance – 05 str. 3/36
Parallel Programs
Parallel Composition
Components concurrently contribute to the transformation of
a computation state.
The meaning comes from interleaving of actions
(transformation steps) of individual components.
Meaning Functions Do Not Compose
Meaning function of a composition cannot be obtain as
composition of meaning functions of participating
components.
The result depends on particular interleaving.
IA169 System Verification and Assurance – 05 str. 4/36
Example of Incomposability
Parallel System
System: (y=x; y++; x=y) (y=x; y++; x=y)
Input-output variable x
Meaning function of both processes is λx->x+1.
The composition is: (λx->x+1)·(λx->x+1).
(λx->x+1)·(λx->x+1) 0 = 2
Two Different System Runs
State = (x, y1, y2)
(0,-,-)
y1=x
−→ (0,0,-)
y2=x
−→ (0,0,0)
y1++
−→
x=y1
−→ (1,1,0)
y2++
−→
x=y2
−→ (1,1,1)
(0,-,-)
y1=x
−→ (0,0,-)
y1++
−→
x=y1
−→ (1,1,-)
y2=x
−→ (1,1,1)
y2++
−→
x=y2
−→ (2,1,2)
IA169 System Verification and Assurance – 05 str. 5/36
Properties of Parallel Programs
Observation
Specific timing of events related to interaction of components
is a form of (part of) input.
Asynchronous parallel system can be viewed as reactive as
there are unknown inputs at the time of execution.
Consequence
For reactive (hence parallel) systems, the intended
behaviour cannot be specified using Hoare triples.
IA169 System Verification and Assurance – 05 str. 6/36
Properties of Parallel/Reactive Programs
Examples of Specification
Events A and B happens before event C.
User is not allowed to enter a new value until the system
processes the previous one.
Procedure X cannot be executed simultaneously by processes
P and Q (mutual exclusion).
Every action A is immediately followed by a sequence of
actions B,C and D.
Turning into Formal Language
Use of Modal and Temporal Logics.
Amir Pnueli, 1977
IA169 System Verification and Assurance – 05 str. 7/36
Deductive Verification for Modal and Temporal Logic
Assumption
System properties are decsribed formally using formulae of
some temporal logic.
Deductive Verification
Approaches similar to the Hoare system exist for temporal
logic formulae, however, they have never been widely used.
Incomposability of meaning functions is difficult to bypass.
Model checking
Alternative way of formal verification of systems.
Based on the state-space exploration.
Allows for specification to be given with formulae of some
temporal logic.
IA169 System Verification and Assurance – 05 str. 8/36
Section
Model Checking
IA169 System Verification and Assurance – 05 str. 9/36
Model Checking
Model Checking – Overview
Build a formal model M of the system under verification.
Express specification as a formula ϕ of selected temporal logic.
Decide, if M |= ϕ. That is, if M is a model of formula ϕ.
(Hence the name.)
Optionally
As a side effect of the decision a counterexample may be
produced.
The counterexample is a sequence of states witnessing
violation (in the case the system is erroneous) of the formula.
Model checking (the decision process) can be fully
automated for all finite (and some infinite) models of
systems.
IA169 System Verification and Assurance – 05 str. 10/36
Model Checking – Schema
Requirements
Specification
Property
Formalization
System
System Model
Model Checking
Simulation
Counterexample
Invalid
Valid
ErrorModelling
IA169 System Verification and Assurance – 05 str. 11/36
Automated Tools for Model Checking
Model Checkers
Software tools that can decide validity of a formula over a
model of system under verification.
SPIN, UppAal, SMV, Prism, DIVINE . . .
Modelling Languages
Processes described as extended finite state machines.
Extension allows to use shared or local variables and guard
execution of a transition with a Boolean expression.
Optionally, some transitions may be synchronised with
transitions of other finite state machines/processes.
IA169 System Verification and Assurance – 05 str. 12/36
Section
Modelling and Formalisation of Verified Systems
IA169 System Verification and Assurance – 05 str. 13/36
Atomic Proposition
Reminder
System can be viewed as a set of states that are walked along
by executing instructions of the program.
State = valuation of modelled variables.
Atomic Propositions
Basic statements describing qualities of individual states, for
example: max(x, y) ≥ 3.
Validity of atomic proposition for a given state must be
decidable with information merely encoded by the state.
Amount of observable events and facts depends on amount of
abstraction used during the system modelling.
IA169 System Verification and Assurance – 05 str. 14/36
Kripke Structure
Kripke Structure
Let AP be a set of atomic propositions.
Kripke structure is a quadruple (S, T, I, s0), where
S is a (finite) set of states,
T ⊆ S × S is a transition relation,
I : S → 2AP
is an interpretation of AP.
s0 ∈ S is an initial state.
Kripke Transition System
Let Act be a set of instructions executable by the program.
Kripke structure can be extended with transition labelling to
form a Kripke Transitions System.
Kripke Transition System is a five-tuple (S, T, I, s0, L), where
(S, T, I, s0) is Kripke Structure,
L : T → Act is labelling function.
IA169 System Verification and Assurance – 05 str. 15/36
Kripke Structure – Example
Kripke Structure
P
P,S,B
P,S,C
Beer
Coke
Payment Choice
AP={P – Paid, S – Served, C – Coke, B – Beer}
IA169 System Verification and Assurance – 05 str. 16/36
Kripke Structure – Example
Kripke Transition System
P
P,S,B
P,S,C
Takes Beer
Takes Coke
Chooses Coke
Chooses BeerGives Coin
Beer
Coke
Payment Choice
AP={P – Paid, S – Served, C – Coke, B – Beer}
IA169 System Verification and Assurance – 05 str. 16/36
System Run
Run
Maximal path (such that it cannot be extended) in the graph
induced by Kripke Structure starting at the initial state.
Let M = (S, T, I, s0) be a Kripke structure. Run is a sequence
of states π = s0, s1, s2, . . . such that ∀i ∈ N0.(si , si+1) ∈ T.
Finite Paths and Runs
Some finite path π = s0, s1, s2, . . . , sk cannot be extended if
sk+1 ∈ S.(sk, sk+1) ∈ T.
Technically, we will turn maximal finite path into infinite by
repeating the very last state.
Maximal path s0, . . . , sk will be understood as infinite run
s0, . . . , sk, sk, sk, . . ..
IA169 System Verification and Assurance – 05 str. 17/36
Implicit and Explicit System Description
Observation
Usually, Kripke structure that captures system behaviour is not
given by full enumeration of states and transitions (explicitly),
but it is given by the program source code (implicitly).
Implicit description tends to be exponentially more succinct.
State-Space Generation
Computation of explicit representation from the implicit one.
Interpretation of implicit representation must be formally
precise.
Practise
Programming languages do not have precise formal semantics.
Model checkers often build on top of modelling languages.
IA169 System Verification and Assurance – 05 str. 18/36
An Example of Modelling Language – DVE
Finite Automaton
States (Locations)
Initial state
Transitions
(Accepting states)
Transitions Extended with
Guards
Synchronisation and
Value Passing
Effect (Assignment)
Local Variables
integer, byte
channel
p1
p4
p2
p3
x==b
b=0,x=0
sync c?x
b=b+1
b=b+1
Process B
byte b,x;
IA169 System Verification and Assurance – 05 str. 19/36
Example of System Described in DVE Language
channel {byte} c[0];
process A {
byte a;
state q1,q2,q3;
init q1;
trans
q1→q2 { effect a=a+1; },
q2→q3 { effect a=a+1; },
q3→q1 { sync c!a; effect a=0; };
}
process B {
byte b,x;
state p1,p2,p3,p4;
init p1;
trans
p1→p2 { effect b=b+1; },
p2→p3 { effect b=b+1; },
p3→p4 { sync c?x; },
p4→p1 { guard x==b; effect b=0, x=0; };
}
system async;
IA169 System Verification and Assurance – 05 str. 20/36
Semantics Shown By Interpretation
State: []; A:[q1, a:0]; B:[p1, b:0, x:0]
0 0.0 : q1 → q2 { effect a = a+1; }
1 1.0 : p1 → p2 { effect b = b+1; }
Command:1
—————————————————————
State: []; A:[q1, a:0]; B:[p2, b:1, x:0]
0 0.0 : q1 → q2 { effect a = a+1; }
1 1.1 : p2 → p3 { effect b = b+1; }
Command:1
—————————————————————
State: []; A:[q1, a:0]; B:[p3, b:2, x:0]
0 0.0 : q1 → q2 { effect a = a+1; }
Command:0
—————————————————————
State: []; A:[q2, a:1]; B:[p3, b:2, x:0]
0 0.1 : q2 → q3 { effect a = a+1; }
Command:0
—————————————————————
State: []; A:[q3, a:2]; B:[p3, b:2, x:0]
0 0.2&1.2 : q3 → q1 { sync c!a; effect a = 0; }
p3 → p4 { sync c?x; }
Command:0
—————————————————————
State: []; A:[q1, a:0]; B:[p4, b:2, x:2]
IA169 System Verification and Assurance – 05 str. 21/36
Section
Formalising System Properties
IA169 System Verification and Assurance – 05 str. 22/36
Specification as Languages of Infinite Words
Problem
How to formally describe properties of a single run?
How to mechanically check for their satisfaction?
Solution
Employ finite automaton as a mechanical observer of run.
Runs are infinite.
Finite automata for infinite words (ω-regular languages).
Büchi acceptance condition – automaton accepts a word if it
passes through an accepting state infinitely many often.
IA169 System Verification and Assurance – 05 str. 23/36
Automata over infinite words
Büchi automata
Büchi automaton is a tuple A = (Σ, S, s, δ, F), where
Σ is a finite set of symbols,
S is a finite set f states,
s ∈ S is an initial state,
δ : S × Σ → 2S
is transition relation, and
F ⊆ S is a set of accepting states.
Language accepted by a Büchi automaton
Run ρ of automaton A over infinite word w = a1a2 . . . is a
sequence of states ρ = s0, s1, . . . such that s0 ≡ s and
∀i : si ∈ δ(si−1, ai ).
inf (ρ) – Set of states that appear infinitely many time in ρ.
Run ρ is accepting if and only if inf (ρ) ∩ F = ∅.
Language accepted with an automaton A is a set of all words
for which an accepting run exists. Denoted as L(A).
IA169 System Verification and Assurance – 05 str. 24/36
Shortcuts in Transition Guards
Observation
Let AP={X,Y,Z}.
Transition labelled with {X} denotes that X must hold true
upon execution of the transition, while Y and Z are false.
If we want to express that X is true, Z is false, and for Y we
do not care, we have to create two transitions labelled with
{X} and {X, Y }.
APs as Boolean Formulae
Transitions between the two same states may be combined
and labelled with a Boolean formula over atomic propositions.
Example
Transitions {X}, {Y}, {X,Y}, {X,Z}, {Y,Z} a {X,Y,Z} can be
combined into a single one labelled with X ∨ Y .
If there are no restrictions upon execution of the transition, it
may be labelled with true ≡ X ∨ ¬X.
IA169 System Verification and Assurance – 05 str. 25/36
Task: Express with a Büchi automaton
System
Vending machine as seen before.
Σ = 2{P,S,C,B},
Paid = {A ∈ Σ | P ∈ A}, Served = {A ∈ Σ | S ∈ A}, . . .
Express the following properties
Vending machine serves at least one drink.
Vending machine serves at least one coke.
Vending machine serves infinitely many drinks.
Vending machine serves infinitely many beers.
Vending machine does not serve a drink without being paid.
After being paid, vending machine always serve a drink.
IA169 System Verification and Assurance – 05 str. 26/36
Section
Linear Temporal Logic
IA169 System Verification and Assurance – 05 str. 27/36
Linear Temporal Logic (LTL) Informally
Formula ϕ
Is evaluated on top of a single run of Kripke structure.
Express validity of APs in the states along the given run.
Temporal Operators of LTL
F ϕ — ϕ holds true eventually (Future).
G ϕ — ϕ holds true all the time (Globally).
ϕ U ψ — ϕ holds true until eventually ψ holds true (Until).
X ϕ — ϕ is valid after execution of one transition (Next).
ϕ R ψ — ψ holds true until ϕ ∧ ψ holds true (Release).
ϕ W ψ — until, but ψ may never become true (Weak Until).
IA169 System Verification and Assurance – 05 str. 28/36
Graphical Representation of LTL Temporal Operators
X ϕ : •−→
ϕ
•−→•−→•−→•−→• · · ·
ϕ U ψ :
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ψ
•−→• · · ·
F ϕ : •−→•−→•−→•−→
ϕ
•−→• · · ·
G ϕ :
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
• · · ·
ϕ R ψ :
ψ
•−→
ψ
•−→
ψ
•−→
ψ
•−→
ϕ∧ψ
• −→• · · · or
ψ
•−→
ψ
•−→
ψ
•−→
ψ
•−→
ψ
•−→
ψ
• · · ·
ϕ W ψ :
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ψ
•−→• · · · or
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
• · · ·
IA169 System Verification and Assurance – 05 str. 29/36
Syntax of LTL
Let AP be a set of atomic propositions.
If p ∈ AP, then p is an LTL formula.
If ϕ is an LTL formula, then ¬ϕ is an LTL formula.
If ϕ and ψ are LTL formulae, then ϕ ∨ ψ is an LTL formula.
If ϕ is an LTL formula, then X ϕ is an LTL formula.
If ϕ and ψ are LTL formulae, then ϕ U ψ is an LTL formula.
Alternatively
ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | X ϕ | ϕ U ϕ
IA169 System Verification and Assurance – 05 str. 30/36
Syntactic shortcuts
Propositional Logic
ϕ ∧ ψ ≡ ¬(¬ϕ ∨ ¬ψ)
ϕ ⇒ ψ ≡ ¬ϕ ∨ ψ
ϕ ⇔ ψ ≡ (ϕ ⇒ ψ) ∧ (ψ ⇒ ϕ)
Temporal operators
F ϕ ≡ true U ϕ
G ϕ ≡ ¬F ¬ϕ
ϕ R ψ ≡ ¬(¬ϕ U ¬ψ)
ϕ W ψ ≡ ϕ U ψ ∨ G ϕ
Alternative syntax
Fϕ ≡ ϕ
Gϕ ≡ ϕ
Xϕ ≡ ◦ϕ
IA169 System Verification and Assurance – 05 str. 31/36
Models of LTL Formulae
Model of an LTL formula
Let AP be a set of atomic propositions.
Model of an LTL formula is a run π of Kripke structure.
Notation
Let π = s0, s1, s2, . . ..
Suffix of run π starting at sk is denoted as
πk = sk, sk+1, sk+2, . . ..
K-th state of the run, is referred to as π(k) = sk.
IA169 System Verification and Assurance – 05 str. 32/36
Semantics of LTL
Assumptions
Let AP be a set of atomic propositions.
Let π be a run of Kripke structure M = (S, T, I, s0).
Let ϕ, ψ be syntactically correct LTL formulae.
Let p ∈ AP denote atomic proposition.
Semantics
π |= p iff p ∈ I(π(0))
π |= ¬ϕ iff π |= ϕ
π |= ϕ ∨ ψ iff π |= ϕ or π |= ψ
π |= X ϕ iff π1
|= ϕ
π |= ϕ U ψ iff ∃k.0 ≤ k, πk
|= ψ and
∀i.0 ≤ i < k, πi
|= ϕ
IA169 System Verification and Assurance – 05 str. 33/36
Semantics of Other Temporal Operators
π |= F ϕ iff ∃k.k ≥ 0, πk
|= ϕ
π |= G ϕ iff ∀k.k ≥ 0, πk
|= ϕ
π |= ϕ R ψ iff (∃k.0 ≤ k, πk
|= ϕ ∧ ψ and
∀i.0 ≤ i < k, πi
|= ψ)
or (∀k.k ≥ 0, πk
|= ψ)
π |= ϕ W ψ iff (∃k.0 ≤ k, πk
|= ψ and
∀i.0 ≤ i < k, πi
|= ϕ)
or (∀k.k ≥ 0, πk
|= ϕ)
IA169 System Verification and Assurance – 05 str. 34/36
LTL Model Checking
Verification Employing LTL
System is viewed as a set of runs.
System is satisfies LTL formula if and only if all system runs
satisfy the formula.
In other words, any run violating the formula is a witness that
the system does not satisfy the formula.
Lemma
If a finite state system does not satisfy an LTL formula then
this may be witnessed with a lasso-shaped run.
Run π is lasso-shaped if π = π1 · (π2)ω, where
π1 = s0, s1, . . . , sk
π2 = sk+1, sk+2, . . . , sk+n, where sk ≡ sk+n.
Note that πω denotes infinite repetition of π.
IA169 System Verification and Assurance – 05 str. 35/36
Homework
Homework
Model Peterson’s mutual exclusion protocol in ProMeLa.
State expected LTL properties of Peterson’s protocol.
Verify them using SPIN model checker.
IA169 System Verification and Assurance – 05 str. 36/36