Fundamental Algorithms for System Modeling, Analysis, and Optimization
Edward A. Lee, Jaijeet Roychowdhury, Sanjit A. Seshia
UC Berkeley EECS 144/244 Fall 2010 Copyright 2010, E. A. Lee, J. Roychowdhury, S. A. Seshia, All rights reserved
Lec 19: Model Checking
Model Checking
G(p X q) Yes, property satisfied
Model Checker
no q p p q
Outline
Computation Tree Logic and why it is useful for model checking Model Checking with BDDs Bounded Model Checking with SAT
Labelled State Transition Graph
pq pq
qr qr r pq r
Kripke structure
. . .
Infinite Computation Tree
4
Temporal Logic
Linear Temporal Logic (LTL) Properties expressed over a single time-line Computation Tree Logic (CTL, CTL*) Properties expressed over a tree of all possible executions CTL* gives more expressiveness than LTL CTL is a subset of CTL* that is easier to verify than arbitrary CTL*
Computation Tree Logic (CTL*)
Introduce two new operators called Path quantifiers A p : Property p holds along all computation paths E p : Property p holds along at least one path Example: From any state, it is possible to get to the reset state
A G ( E F reset )
CTL: Every F, G, X, U must be preceded by either an A or aE
E.g., Cant write A (FG p)
LTL is just like having an A on the outside
6
Why CTL?
Verifying LTL properties turns out to be computationally harder than CTL Exponential in the size of the LTL expression
linear for CTL
For both, verification is linear in the size of the state graph
CTL as a way to approximate LTL
AG EF p is weaker than G F p
Good for finding bugs...
AF AG p is stronger than F G p
Good for verifying correctness...
CTL Model Checking
So, weve decided to do CTL model checking. What are the algorithms?
Recap: Reachability Analysis
Given: 1. A Boolean formula corresponding to initial states R0 2. To find: All states reachable from R0 in 1, 2, 3, transitions (clock ticks) Strategy: Denote set of states reachable from R0 in k (or less) clock ticks as Rk Rk+1(s+) = Rk(s+) + s { Rk(s) . (s, s+) }
10
Backwards Reachability Analysis
Given: 1. A Boolean formula corresponding to error states E0 2. To find: All states that can reach E0 in 1, 2, 3, transitions (clock ticks) Strategy: Denote set of states reachable from E0 in k (or less) clock ticks as Ek Ek+1(s) = Ek(s) + s+ { Ek(s+) . (s, s+) }
11
Verification of G p
Corresponding CTL formula is AGp
Remember that p is a function of s
Forward Reachability Analysis:
Check if any Rk(s) . p(s) is true for any s
Backward Reachability Analysis:
Set E0 = p Check if Ek(s) . R0(s) is true for any s
12
Model Checking Arbitrary CTL
Need only consider the following types of CTL properties: EXp EGp E(pUq) Why? all others are expressible using above AGp=? AG(p (AFq))=?
13
Model Checking CTL Properties
We define a general recursive procedure called Check to do this
Performs fixpoint computation
Definition of Check:
Input: A CTL property (and implicitly, ) Output: A Boolean formula B representing the set of states satisfying
If B(s) . R0(s) != 0, then is true (in the initial state)
14
The Check procedure
Cases: If is a Boolean formula, then Check() = Else: = EX p, then Check() = CheckEX(Check(p)) = E(p U q), then Check() = CheckEU(Check(p), Check(q)) = E G p, then Check() = CheckEG(Check(p)) Note: What are the arguments to CheckEX, CheckEU, CheckEG? CTL properties?
15
CheckEX
CheckEX(p) returns a set of states such that p is true in their next states How to write this?
16
CheckEU
CheckEU(p, q) returns a set of states, each of which is such that Either q is true in that state Or p is true in that state and you can get from it to a state in which p U q is true Seems like circular reasoning! But it works out: using an recursive computation like in reachability analysis
We compute a series of approximations leading to the right answer
17
CheckEU
CheckEU(p, q) returns a set of states, each of which is such that Either q is true in that state Or p is true in that state and you can get from it to a state in which p U q is true Let Z0 be our initial approximation to the answer to CheckEU(p, q) Zk(s) = { q(s) + [ p(s) . x,s+ { (s, x, s+) . Zk-1(s+) } ] } Whats a good choice for Z0? Why will this terminate?
18
Summary
EGp computed similarly Definition of Check:
Input: A CTL property (and implicitly, ) Output: A Boolean formula B representing the set of states satisfying
All Boolean formulas represented symbolically as BDDs
Symbolic Model Checking
19
Bounded Model Checking
Given
[Biere, Clarke, Cimatti, Zhu99]
A finite state machine M (transition system) A property p Determine Does M allow a counterexample to p of k transitions or fewer? This problem can be translated to a SAT problem
20
Models
Transition system described by a set of constraints g=ab g a b Model: c' = p p c } C={ g = a b, p = g c, c' = p
p=gc
Each circuit element is a constraint note: a = at and a' = at+1
21
Properties
We restrict our attention to safety properties. Characterized by:
Initial condition R0 Final condition E (representing error" states)
A counterexample is a path from a state satisfying R0 to state satisfying E, where every transition satisfies C.
22
Unfolding
Unfold the model k times: Uk = C0 C1 ... Ck-1 R0
a b g p c a b g p c
...
a b
g p c
Ek
Use SAT solver to check satisfiability of
R0 Uk Ek
A satisfying assignment is a counterexample of k steps
23
BMC applications
Debugging:
Can find counterexamples using a SAT solver
Proving properties:
Only possible if a bound on the length of the shortest counterexample is known. I.e., we need a diameter bound. The diameter is the maximum length of the shortest path between any two states. Worst case is exponential. Obtaining better bounds is sometimes possible, but generally intractable.
24
New Developments in SAT-based MC
SAT-based bounded model checking has scaled to thousands of state bits and is very useful for debugging
Can verify LTL properties too
Unbounded model checking is now also possible with SAT
interpolation-based model checking
But on some problems, BDD-based model checking is still better
25
