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 and applicable to closed
programs only.
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 formal verification process for ...
... reactive systems.
... parallel/distributed systems.
IA169 System Verification and Assurance – 04 str. 2/36
Section
Verification of Reactive and Parallel Programs
IA169 System Verification and Assurance – 04 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 – 04 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 – 04 str. 5/36
Consequence of Incomposability
Consequence 1
In general, we cannot deduce correctness of the system from
the correctness of its components.
Consequence 2
In general, we cannot decompose the problem of checking
correctness of the system into subproblems, i.e. to reduce it
to the verification of correctness of all the participating
system components.
IA169 System Verification and Assurance – 04 str. 6/36
Specification for Reactive/Parallel Programs
Problem of Specification
The number of inputs and the input values are unknown
before a particular execution of a reactive system.
How to specify the system properties?
Examples of Specification
The system will not crash.
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.
IA169 System Verification and Assurance – 04 str. 7/36
Model Checking Principles
Model Checking
Approach to formal verification of systems.
Based on the system’s state-space exploration.
State-space Exploration
Generate and explore all possible states of computation the
system under verification may get to.
Requires description of system behavior (code, or model).
Requires description of possible input actions (environment).
System Specification
Amir Pnueli, 1977
Specification may be given with logic formulae.
Use of Modal and Temporal Logics
IA169 System Verification and Assurance – 04 str. 8/36
Section
Model Checking
IA169 System Verification and Assurance – 04 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 – 04 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 – 04 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 – 04 str. 12/36
Section
Modelling and Formalization of Verified Systems
IA169 System Verification and Assurance – 04 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 – 04 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 – 04 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 – 04 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 – 04 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 – 04 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.
Practice
Programming languages do not have precise formal semantics.
Model checkers often build on top of modelling languages.
IA169 System Verification and Assurance – 04 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 – 04 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 – 04 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 – 04 str. 21/36
Section
Formalizing System Properties
IA169 System Verification and Assurance – 04 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 – 04 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 – 04 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 – 04 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 – 04 str. 26/36
Section
Linear Temporal Logic
IA169 System Verification and Assurance – 04 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 – 04 str. 28/36
Graphical Representation of LTL Temporal Operators
X ϕ : •−→
ϕ
•−→•−→•−→•−→• · · ·
ϕ U ψ :
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ψ
•−→• · · ·
F ϕ : •−→•−→•−→•−→
ϕ
•−→• · · ·
G ϕ :
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
• · · ·
ϕ R ψ :
ψ
•−→
ψ
•−→
ψ
•−→
ψ
•−→
ϕ∧ψ
• −→• · · · or
ψ
•−→
ψ
•−→
ψ
•−→
ψ
•−→
ψ
•−→
ψ
• · · ·
ϕ W ψ :
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ψ
•−→• · · · or
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
• · · ·
IA169 System Verification and Assurance – 04 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 – 04 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 – 04 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 – 04 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 – 04 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 – 04 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 – 04 str. 35/36
Self-study
Get acquainted with famous SPIN model checker
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 – 04 str. 36/36