Introduction to Model Checking and its
Applications
Cindy Eisner
Formal Methods Group
IBM Labs in Haifa
© 2004 IBM Corporation
IBM Labs in Haifa
Overview
What is model checking?
Symbolic model checking
Applications of symbolic model checking
Conclusion
2
© 2004 IBM Corporation
IBM Labs in Haifa
What is model checking?
3
© 2004 IBM Corporation
IBM Labs in Haifa
Model checking?
Given a model M and a temporal logic formula f, decide if M |= p
Formally:
A model is a quintuple (S, S0, R, P, L)
S is a finite set of states
S0 is a subset of S
R is the transition relation, a subset of S x S
P is a non-empty set of atomic propositions
L is the valuation, a function S -> 2P
We use the temporal logic PSL, a soon-to-be IEEE standard
In the interest of time, we will continue informally
4
© 2004 IBM Corporation
IBM Labs in Haifa
An example
Given
The following model:
1
0
4
request
2
process
request
6
5
3
The PSL formula:
G (request -> X[1..3] process)
(if a request is received, it must be processed within 3 cycles)
Determine whether the model satisfies the formula
5
© 2004 IBM Corporation
IBM Labs in Haifa
CTL Model Checking
Clarke, Emerson (1981)
A branching time temporal logic
PSL model checking can be reduced to CTL model checking
(sometimes the model must be augmented with an automaton)
Idea: unwind state graph to obtain infinite computation tree, reason
about (infinite) paths in the computation tree
FSM
6
Infinite Computation Tree
© 2004 IBM Corporation
IBM Labs in Haifa
CTL
Path Quantifiers
A – for all paths
E – there exists a path
Tense Operators
Xp
- p holds at the next cycle
Fp
- p holds sometime in the future
Gp
- p holds globally in the future
p U q - p holds until q holds
Temporal operators
AX, AF, AG, AU, EX, EF, EG, EU
7
© 2004 IBM Corporation
IBM Labs in Haifa
CTL (continued)
EG p
AF p
AG AF p
8
© 2004 IBM Corporation
IBM Labs in Haifa
CTL Model Checking – Image and Pre-Image
1
0
4
request
2
process
request
6
5
3
Forward traversal: image
Backward traversal: pre-image
9
© 2004 IBM Corporation
IBM Labs in Haifa
CTL Model Checking - EX
ex(set_of_states p)
{
return(PreImg(p));
}
p
0
p
1
p
2
3
p = {0,1,2}
PreImg(p) = {0,1}
EX p = {0,1}
10
© 2004 IBM Corporation
IBM Labs in Haifa
CTL Model Checking - EG
eg(set_of_states p)
{
set_of_states oldY = {};
set_of_states Y = p;
while (Y != oldY) {
oldY = Y;
Y = intersection(Y, ex(Y));
}
return(Y);
}
p
0
1.
2.
3.
4.
p
1
p
2
3
oldY={}; Y={0,1,2};
oldY={0,1,2}; ex(Y)={0,1}; Y={0,1};
oldY={0,1}; ex(Y)={0}; Y = {0};
oldY={0}; ex(Y)={0}; Y={0};
EG p = {0}
11
© 2004 IBM Corporation
IBM Labs in Haifa
CTL Model Checking in Practice
Bare model checking is a nice theory, but
In practice, models are huge
If we limit our integers to 2
bits, then an explicit model
for getmax() has 128 states
2 bits for max
2 bits for a
3 bits for pc
Enter symbolic model checking
12
0
1
2
3
4
5
6
7
getmax () {
int max, a;
a = max = 0;
do {
if (a > max)
max = a;
a = input();
} while (a);
return(max);
}
© 2004 IBM Corporation
IBM Labs in Haifa
Symbolic Model Checking
13
© 2004 IBM Corporation
IBM Labs in Haifa
Symbolic model checking (McMillan 1992)
Use BDDs to:
Implicitly traverse the state space without building the model
Deal simultaneously with sets of states
14
© 2004 IBM Corporation
IBM Labs in Haifa
BDDs (Bryant 1986)
Binary decision diagram
Directed acyclic graph representing a (boolean) function
15
© 2004 IBM Corporation
IBM Labs in Haifa
BDDs (continued)
BDDs are a canonical representation if:
An order is imposed on the variables
Isomorphic sub-trees are combined into a single tree
Nodes whose two children are isomorphic are removed
16
© 2004 IBM Corporation
IBM Labs in Haifa
Logic Operations on BDDs
By Shannon’s expansion
17
© 2004 IBM Corporation
IBM Labs in Haifa
BDDs in Symbolic Model Checking
Functions
Sets of states
Transition relation
18
© 2004 IBM Corporation
IBM Labs in Haifa
Symbolic model checking - example
Design is completely deterministic, but
Inputs behave non-deterministically
Therefore, the model will be non-deterministic
19
© 2004 IBM Corporation
IBM Labs in Haifa
Symbolic model checking – example (continued)
Let’s see how to traverse this model without actually building it
20
© 2004 IBM Corporation
IBM Labs in Haifa
BDDs represent functions
21
© 2004 IBM Corporation
IBM Labs in Haifa
BDDs Represent Sets of States
22
© 2004 IBM Corporation
IBM Labs in Haifa
Transition relation
23
© 2004 IBM Corporation
IBM Labs in Haifa
Building transition relation per bit
24
© 2004 IBM Corporation
IBM Labs in Haifa
BDDs represent transition relation
25
© 2004 IBM Corporation
IBM Labs in Haifa
BDDs represent transition relation (continued)
26
© 2004 IBM Corporation
IBM Labs in Haifa
Computing the Image with the TR
27
© 2004 IBM Corporation
IBM Labs in Haifa
Computing the Image (continued)
28
© 2004 IBM Corporation
IBM Labs in Haifa
Sanity check
We started these initial states:
We took one symbolic step in this design:
And we ended up at this set of states:
And we did it all without building this:
29
© 2004 IBM Corporation
IBM Labs in Haifa
Other methods of model checking
McMillan’s BDD-based method is just one way to do symbolic model
checking
Other techniques include:
SAT-based methods
BDD-based unfolding
Reachability-based on-the-fly methods
Localization
And many many more
And then there is explicit-state model checking
30
© 2004 IBM Corporation
IBM Labs in Haifa
Applications of Symbolic Model Checking
31
© 2004 IBM Corporation
IBM Labs in Haifa
Applications: Hardware Design and Verification (RuleBase)
Mainstream hardware design and verification tool
High-level development of abstract architectural models
Block-level verification of RTL
Active area of research and development
Reductions, abstractions, new symbolic algorithms
Recent tapeouts supported by RuleBase
IBM’s high-end microprocessors and ASICs
STMicroelectronics – ST100® DSP Cores
Marvell – DiscoveryTM System Controllers
Analog Devices – TigerSHARC® Processor
32
© 2004 IBM Corporation
IBM Labs in Haifa
Applications: Software verification (Wolf)
getmax () {
0
1
2
3
4
5
6
7
int max, a;
a = max = 0;
do {
if (a > max)
max = a;
a = input();
} while (a);
return(max);
}
Prototype software verification tool
Active area of research and development
Adaptation of standard techniques
Dedicated software techniques
Recent applications of Wolf:
Discovery of data race in Linux driver
Discovery of out-of-bound access to array in firmware from the
server group due to bad return value from function
33
© 2004 IBM Corporation
IBM Labs in Haifa
Applications: Analysis of Hybrid Control Systems
Beta-level tool for design of nonlinear control systems
Discretize Matlab models to create RuleBase input
Temporal logic formula states that values of control parameters do not exist
Counter-example provides desired values of control parameters
Active area of research and development
Recent case study:
Analysis of system for tracking and intercepting a maneuvering target
Discovery of robust control parameters for the guidance law and extended
Kalman filter
34
© 2004 IBM Corporation
IBM Labs in Haifa
Non-traditional applications
Railway interlockings
Does the interlocking prevent two trains from
being on the same piece of track at the same
time?
Firefly game
How many initial states converge, and are there
board sizes for which no converging initial states
exist?
Various amusing NP-complete problems
There is no free lunch: finding a Hamiltonian
circuit is difficult for even small graphs
On a lazy Thursday afternoon, it is sometimes
interesting to see how far you can push the tools
35
© 2004 IBM Corporation
IBM Labs in Haifa
Conclusion
36
© 2004 IBM Corporation
IBM Labs in Haifa
Conclusion
Model checking is a fascinating area of research, with many practical
applications
Find out more by visiting our home page:
www.haifa.il.ibm.com/projects/verification/Formal_Methods-Home/index.html
37
© 2004 IBM Corporation