Introduction Modeling Specification Algorithms Conclusions
Formal Verification, Model Checking
Radek Pelánek
Introduction Modeling Specification Algorithms Conclusions
Motivation
Formal Methods: Motivation
examples of what can go wrong – first lecture
non-intuitiveness of concurrency (particularly with shared
resources)
mutual exclusion
adding puzzle
Introduction Modeling Specification Algorithms Conclusions
Motivation
Formal Methods
Formal Methods
‘Formal Methods’ refers to mathematically rigorous techniques
and tools for
specification
design
verification
of software and hardware systems.
Introduction Modeling Specification Algorithms Conclusions
Motivation
Formal Verification
Formal Verification
Formal verification is the act of proving or disproving the
correctness of a system with respect to a certain formal
specification or property.
Introduction Modeling Specification Algorithms Conclusions
Motivation
Formal Verification vs Testing
formal verification testing
finding bugs medium good
proving correctness good -
cost high small
Introduction Modeling Specification Algorithms Conclusions
Motivation
Types of Bugs
likely rare
harmless testing not important
catastrophic testing, FV FV
Introduction Modeling Specification Algorithms Conclusions
Motivation
Formal Verification Techniques
manual human tries to produce a proof of correctness
semi-automatic theorem proving
automatic algorithm takes a model (program) and a
property; decides whether the model satisfies
the property
We focus on automatic techniques.
Introduction Modeling Specification Algorithms Conclusions
Motivation
Application Domains of FV
generally safety-critical systems: a system whose failure
can cause death, injury, or big financial loses (e.g.,
aircraft, nuclear station)
particularly embedded systems
often safety critical
reasonably small and thus amenable to formal
verification
Introduction Modeling Specification Algorithms Conclusions
Motivation
Well Known Bugs
Ariane 5 explosion on its first flight; caused by reuse of
some parts of a code from its predecessor without
proper verification
Therac-25 radiation therapy machine; due to a software
error, six people are believed to die because of
overdoses
Pentium FDIV design error in a floating point division unit;
Intel was forced to offer replacement of all flawed
processors
Introduction Modeling Specification Algorithms Conclusions
Motivation
Outlook
this lecture (foundations):
basics of a model checking technique
overview of modeling formalisms, logics
basic algorithms
next lectures (real-time, applications):
theory: timed automata
extensions for practical modeling
verification tool Uppaal
case studies, realistic examples
Introduction Modeling Specification Algorithms Conclusions
Motivation
Goal of the Lecture
goal: to understand the basic principles of model
checking technique
important for efficient use of a model checking tool
Introduction Modeling Specification Algorithms Conclusions
Motivation
Overlap with Other Courses
IV113 Introduction to Validation and Verification
IA159 Formal Verification Methods
IA040 Modal and Temporal Logics for Processes
IA006 Selected topics on automata theory
verification in this course:
foundations only briefly
real-time aspects
Introduction Modeling Specification Algorithms Conclusions
Motivation
Contents
2 Modeling
Guarded Command Language
Finite State Machines
Other Modeling Formalisms
3 Specification
Types of Properties
Temporal Logics
Timed Logics
4 Algorithms
State Space Search
Logic Verification
State Space Explosion
Introduction Modeling Specification Algorithms Conclusions
Model Checking
Model Checking
automatic verification technique
user produces:
a model of a system
a logical formula which describes the desired properties
model checking algorithm:
checks if the model satisfies the formula
if the property is not satisfied, a counterexample is
produced
Introduction Modeling Specification Algorithms Conclusions
Model Checking
Model Checking (cont.)
specification system
temporal logic formal
KKKKK model
KKKK x
KKKK xxxx
KKKK
KKKK x
xxxxxx
KKKK xxx
KKKK
KKKK xxxxxxx
KKK x
xx
!) w xxx
model checking
Introduction Modeling Specification Algorithms Conclusions
Model Checking
State Space
model checking algorithms are based on state space
exploration, i.e., “brute force”
state space describes all possible behaviours of the model
state space ∼ graph:
nodes = states of the system
edges = transitions of the system
in order to construct state space, the model must be
closed, i.e., we need to model environment of the system
Introduction Modeling Specification Algorithms Conclusions
Model Checking
Example: Model and State Space
Introduction Modeling Specification Algorithms Conclusions
Model Checking
Model Checking: Steps
1 modeling: system → model
2 specification: natural language specification → property
in formal logic
3 verification: algorithm for checking whether a model
satisfies a property
Introduction Modeling Specification Algorithms Conclusions
Modeling Formalisms
guarded command language simple low level modeling
language
finite state machines usually extended with variables,
communication
Petri Nets graphical modeling language
process algebra infinite state systems
timed automata focus of the next lecture
Introduction Modeling Specification Algorithms Conclusions
Guarded Command Language
Guarded Command Language
the simplest modeling language
not useful for actual modeling
simple to formalize
we discuss formal syntax and semantics
foundation for later discussion of timed automata
Introduction Modeling Specification Algorithms Conclusions
Guarded Command Language
Guarded Command Language
integer variables
rules:
if condition then update
conditions: boolean expressions over variables
updates: sequences of assignments to variables
Introduction Modeling Specification Algorithms Conclusions
Guarded Command Language
Example
a : if x = 0 then x := 1
b : if y < 2 then y := y + 1
c : if x = 1 ∧ y ≥ 1 then x := 0, z := 1
Notes:
this is an artificial example (does not model anything
meaningful)
a, b, c are names of actions
no control flow
rules executed repeatedly
initial state: x = 0, y = 0, z = 0
Introduction Modeling Specification Algorithms Conclusions
Guarded Command Language
Syntax
let V be a finite set of integer variables
expressions over V are defined using standard boolean
(=, <) and binary (+, −, ·, ...) operations
model is a tuple M = (V , E )
E = {t1 , . . . , tn } is a finite set of transitions, where
ti = (gi , ui ):
predicate gi (a boolean expression over V )
update ui (~x ) (a sequence of assignments over V )
Introduction Modeling Specification Algorithms Conclusions
Guarded Command Language
Semantics
The semantics of model M is a state space (formally called
Kripke structure) JMK = (S, →, s0 , L) where
states S are valuations of variables, i.e., V → Z
s → s 0 iff there exists (gi , ui ) ∈ T such that
s ∈ Jgi K, s 0 = ui (s)
semantics Jgi K of guards and ui (s) is the natural one
s0 is the zero valuation (∀v ∈ V : s0 (v ) = 0)
Introduction Modeling Specification Algorithms Conclusions
Guarded Command Language
Example
a : if x = 0 then x := 1
b : if y < 2 then y := y + 1
c : if x = 1 ∧ y ≥ 1 then x := 0, z := 1
Construct the state space.
Introduction Modeling Specification Algorithms Conclusions
Guarded Command Language
Example
a : if x = 0 then x := 1
b : if y < 2 then y := y + 1
c : if x = 1 ∧ y ≥ 1 then x := 0, z := 1
Introduction Modeling Specification Algorithms Conclusions
Guarded Command Language
Application
simple to formalize, powerful (Turing power)
not suitable for “human” use
some simple protocols can be modeled
control flow – variable pc (program counter)
Introduction Modeling Specification Algorithms Conclusions
Guarded Command Language
Example: Ticket Protocol
Introduction Modeling Specification Algorithms Conclusions
Guarded Command Language
Example: Ticket Protocol
pc1 := 0; pc2 := 0;
t := 0; s := 0; a1 := 0; a2 := 0;
pc1 = 0 -> pc1 := 1, a1 := t, t := t + 1;
pc1 = 1 && a1 <= s -> pc1 := 2;
pc1 = 2 -> pc1 := 0, s := s + 1;
pc2 = 0 -> pc2 := 1, a2 := t, t := t + 1;
pc2 = 1 && a2 <= s -> pc2 := 2;
pc2 = 2 -> pc2 := 0, s := s + 1;
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Extended Finite State Machines
each process (thread) is modelled as one finite state
machine (machine state = process program counter)
machines are extended with variables:
local computation: guards, updates
shared memory communication
automata can communicate via channels (with value
passing):
handshake (rendezvous, synchronous communication)
asynchronous communication via buffers
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Example: Peterson’s Algorithm
flag[0], flag[1] (initialed to false) — meaning I
want to access CS
turn (initialized to 0) — used to resolve conflicts
Process 0: Process 1:
while (true) { while (true) {
<noncritical section>; <noncritical section>;
flag[0] := true; flag[1] := true;
turn := 1; turn := 0;
while flag[1] and while flag[0] and
turn = 1 do { }; turn = 0 do { };
<critical section>; <critical section>;
flag[0] := false; flag[1] := false;
} }
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Example: Peterson’s Algorithm
Exercise: create a model of Peterson’s Algorithm using
extended finite state machines, i.e., of the following type:
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Example: Peterson’s Algorithm
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Art of Modeling
choosing the right level of abstraction
depends on purpose of the model, assumption about the
system, ...
example: if x == 0 then x := x + 1
one atomic transition
two transitions: test, update (allows interleaving)
multiple “assembler level” transitions: if, load, add, store
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
EFSM: Semantics
formal syntax and semantics defined in similar way as for
guarded command language
just more technical, basic idea is the same
note: state space can be used to reason about the model
– e.g., to prove mutual exclusion requirements (cf.
Assignment 1)
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Example: Peterson’s Algorithm
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Example: Communication Protocol
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Example: Elevator
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Example: Elevator
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Application: Verification of Link Layer Protocol
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Layer Link Protocol of the IEEE-1394
model of the “FireWire” high performance serial bus
n nodes connected by a serial line
protocol consists of three stack layers:
the transaction layer
the link layer
the physical layer
link layer protocol – transmits data packets over an
unreliable medium to a specific node or to all nodes
(broadcast)
transmission can be performed synchronously or
asynchronously
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Notes
link layer
main focus of verification
modeled in high detail
transportation layer, physical layer (bus)
“environment” of link layer
modeled only abstractly
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Introduction Modeling Specification Algorithms Conclusions
Finite State Machines
Introduction Modeling Specification Algorithms Conclusions
Other Modeling Formalisms
Timed Automata
extension of finite state machines with clocks (continuous
time)
next lecture
Introduction Modeling Specification Algorithms Conclusions
Other Modeling Formalisms
Petri Nets: Small Example
graphical formalism (place, transitions, tokens)
Introduction Modeling Specification Algorithms Conclusions
Other Modeling Formalisms
Petri Nets: Realistic Model
Introduction Modeling Specification Algorithms Conclusions
Other Modeling Formalisms
Process Algebra
a
A −→ XX
b
X −→ A k B
basic process algebra (BPA), basic parallel processes
(BPP)
infinite state system modeling (e.g., recursion)
mainly theoretical research
Introduction Modeling Specification Algorithms Conclusions
Specification of Properties
properties the verified system should satisfy
expressed in a formal logic
Introduction Modeling Specification Algorithms Conclusions
Types of Properties
Safety and Liveness
safety liveness
“nothing bad ever hap- “something good eventu-
pens” ally happens”
example: error state is example: when a request
never reached is issued, eventually a re-
sponse is generated
verification = reachability verification = cycle detec-
problem, find a run which tion, find a run in which
violates the property the ‘good thing’ is post-
poned indefinitely
Introduction Modeling Specification Algorithms Conclusions
Types of Properties
Examples of Safety Properties
no deadlock
mutual exclusion is satisfied
a corrupted message is never marked as a good one
the wheels are in a ready position during the landing
Introduction Modeling Specification Algorithms Conclusions
Types of Properties
Examples of Liveness Properties
each process can eventually access critical section
each request will be satisfied
a message is eventually transmitted
there will be always another sunrise
Introduction Modeling Specification Algorithms Conclusions
Temporal Logics
Temporal Logic
temporal logic is a formal logic used to reason about
sequences of events
there are many temporal logics (see the course IA040)
the main classification: linear X branching
Introduction Modeling Specification Algorithms Conclusions
Temporal Logics
Linear Temporal Logic (LTL)
Xφ neXt
Fφ Future
Gφ Globally
ψ U φ Until
Introduction Modeling Specification Algorithms Conclusions
Temporal Logics
LTL: Examples
a message is eventually transmitted F transmit
each request will be satisfied G (request ⇒ F response)
there will be always another sunrise G F sunrise
the road will be dry until it rains dry U rains
process waits until it access CS wait U CS
Introduction Modeling Specification Algorithms Conclusions
Temporal Logics
LTL: Examples
What is expressed by these formulas? For each formula draw a
sequence of states such that the formula is a) satisfied, b) not
satisfied.
GFa
FGa
G(a ⇒ Fb)
aU(bUc)
(aUb)Uc
Introduction Modeling Specification Algorithms Conclusions
Timed Logics
Timed Logics
classical temporal logics
good for reasoning about sequences of states
may be insufficient for dealing with real time
real time extensions
Introduction Modeling Specification Algorithms Conclusions
Timed Logics
Metric Interval Temporal Logic (MITL)
extension of LTL
temporal operator can be restricted to certain interval
examples:
G(req ⇒ F≤3 serv )
any request will be serviced within three time units
dry U[12,14] rains
after lunch it will rain, until that the road will be dry
Introduction Modeling Specification Algorithms Conclusions
Timed Logics
Specification in Practice
timed logics – mainly theoretical research
practical specification of properties:
classical temporal logics
often limited subset or only specific patterns
Introduction Modeling Specification Algorithms Conclusions
State Space Search
State Space Search
construction of the whole state space
verification of simple safety properties (e.g., mutual
exclusion) = basically classical graph traversal
(breadth-first or depth-first search)
graph is represented implicitly = constructed on-demand
from the model (description)
Introduction Modeling Specification Algorithms Conclusions
Logic Verification
Logic Verification
transformation to automata
Buchi automaton: finite automaton over infinite words
a word is accepted if the run of the automaton visits an
accepting state infinitely often (compare with a final state
for finite words)
Introduction Modeling Specification Algorithms Conclusions
Logic Verification
Example
property: G(req ⇒ Fserv )
negation: F(req ∧ G¬serv )
Introduction Modeling Specification Algorithms Conclusions
Logic Verification
Product Automaton
property φ → automaton for the negation of the property
A¬φ
state space of the model S + automaton A¬φ → product
automaton S × A¬φ
product automaton represents erroneous runs
Introduction Modeling Specification Algorithms Conclusions
Logic Verification
Product Automaton: Emptiness Check
model satisfies property ⇔ the language of the product
automaton is empty
verification is reduced to non-emptiness check of product
automaton
Buchi automata: non-emptiness check is performed by
(accepting) cycle detection
Introduction Modeling Specification Algorithms Conclusions
State Space Explosion
State Space Explosion
size of the state space grows very quickly (with respect to
size of the model)
the worst case: exponential increase (next slide)
theory: most interesting model checking problems are
PSPACE-complete
practice: the worst case does not occur, nevertheless
memory/time requirements are very high
Introduction Modeling Specification Algorithms Conclusions
State Space Explosion
Example
For n processes the number of states is 2n + n · 2n−1 .
Introduction Modeling Specification Algorithms Conclusions
State Space Explosion
Dealing with State Space Explosion
abstraction
reduction techniques
efficient implementations
Introduction Modeling Specification Algorithms Conclusions
State Space Explosion
Abstraction
data abstraction (e.g., instead of N use {blue, red})
automated abstraction
abstract - model check - refine
Introduction Modeling Specification Algorithms Conclusions
State Space Explosion
Reduction Techniques
symmetry – consider only one of symmetric states
partial order – consider only one of equivalent
interleavings
compositional construction – build the state space in steps
Introduction Modeling Specification Algorithms Conclusions
State Space Explosion
Efficient Implementations
efficient representation of states, sets of states (symbolic
methods — Binary Decision Diagrams)
low level optimizations (e.g. memory management)
distributed algorithms on networks of workstations
randomization, heuristics – guiding toward errors
Introduction Modeling Specification Algorithms Conclusions
Model Checking: History
80’: basic algorithms, automata theory, first simple tools,
small examples
early 90’: reduction techniques, efficient versions of first
tools, applications to protocol verification
late 90’: extensions (timed, probabilistic), first
commercial applications for hardware verification
state of the art: automatic abstraction, combination with
other techniques, research tools for software verification,
hardware verification widely adopted
Introduction Modeling Specification Algorithms Conclusions
Summary
formal verification
model checking: modeling, specification, verification
modeling formalisms: guarded command language, finite
state machines, Petri nets, ...
formal property specification: temporal logics
algorithms: state space search, Buchi automata,
techniques for reducing state space explosion
