This preview shows page 1-2-15-16-17-32-33 out of 33 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 33 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 33 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 33 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 33 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 33 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 33 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 33 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 33 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Lecture 4: Symbolic Model Checking with BDDsEdmund M. Clarke, Jr.Computer Science DepartmentCarnegie Mellon UniversityPittsburgh, PA 15213Temporal Logic Model CheckingSpecification Language: A propositional temporal logic.Verification Procedure: Exhaustive search of the state space of the concurrent systemto determine truth of specification.• E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons forbranching time temporal logic. In Logic of programs: workshop, Yorktown Heights,NY, May 1981, volume 131 of Lecture Notes in Computer Science. Springer-Verlag,1981.• J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems inCESAR. In Proceedings of the Fifth International Symposium in Programming,volume 137 of Lecture Notes in Computer Science. Springer-Verlag, 1981.Why Model Checking?Advantages:• No proofs!!!• Fast• Counterexamples• No problem with partial specifications• Logics can easily express many concurrency propertiesMain Disadvantage:State Explosion Problem• Too many processes• In digital hardware terms: too many latchesMuch progress recently!!Temporal Logica bb cca ba bcccb cState Transition Graph orKripke Model(Unwind State Graph to obtain Infinite Tree)Infinite Computation TreeComputation Tree LogicsFormulas are constructed from path quantifiers and temporal operators:1.Path quantifier:• A—“for every path”• E—“there exists a path”2.Temporal Operator:• Xp—p holdsnext time.• Fp—p holds sometime in the future• Gp—p holds globally in the future• pUq—p holdsuntil q holdsThe Logic CTLIn CTL each temporal operator must be immediately preceeded by a path quantifier.The four most widely used CTL operators are illustrated below. Each computation treehas initial state s0as its root.g............ggggg g g............ggM, s0|= AGg M, s0|= AFgg............g............ggM, s0|= EFg M, s0|= EGgTypical CTL Formulas• EF(Started ∧ ¬Ready): it is possible to get to a state where Started holds butReady does not hold.•AG(Req ⇒ AFAck): if a Request occurs, then it will be eventually Acknowledged.•AG(AF DeviceEnabled): DeviceEnabled holds infinitely often on everycomputation path.•AG(EF Restart): from any state it is possible to get to the Restart state.Model Checking ProblemLet M be the state–transition graph obtained from the concurrent system.Let f be the specification expressed in temporal logic.Find all states s of M such thatM, s |= fand check if initial states are among these.Efficient model checking algorithms exist for CTL.• E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-stateconcurrent systems using temporal logic specifications. ACM Trans. ProgrammingLanguages and Systems, 8(2):pages 244–263, 1986.Explicit TraversalPreprocessorModel Checker(EMC)CTL formulasState Transition Graph10 to 10 states45True or CounterexampleSymbolic Model CheckingMethod used by most “industrial strength” model checkers:• uses boolean encoding for state machine and sets of states.• can handle much larger designs – hundreds of state variables.• BDDs traditionally used to represent boolean functions.Symbolic Model Checking with BDDsKen McMillan implemented a version of the CTL model checking algorithm usingBinary Decision Diagrams in 1987.Carl Pixley independently developed a similar algorithm, as did the Frenchresearchers, Coudert and Madre.BDDs enabled handling much larger concurrent systems. (usually, anorder ofmagnitude increasein hardware latches!)• J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolicmodel checking: 1020states and beyond. Information and Computation,98(2):pages 142–170, 1992.• K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Fixpoint AlgorithmsEFp = p ∨ EXEFpppFixpoint Algorithms (cont.)Key properties of EFp:1. EFp = p ∨ EXEFp2. U = p ∨ EXU implies EFp ⊆ UWe write EFp = Lfp U.p ∨ EXU.How to compute EFp:U0= FalseU1= p ∨ EXU0U2= p ∨ EXU1U3= p ∨ EXU2...M, s0|= EFp?sp0U0= ∅M, s0|= EFp?sp0U1= p ∨ EXU0M, s0|= EFp?sp0U2= p ∨ EXU1M, s0|= EFp?sp0U3= p ∨ EXU2Ordered Binary Decision Trees and DiagramsOrdered Binary Decision Tree for the two-bit comparator, given by the formulaf(a1, a2, b1, b2) = (a1↔ b1) ∧ (a2↔ b2),is shown in the figure below:ba21ba2bba21ba2bba21ba2bba21ba2b222 2222 2a2a2a2a2b1b1a11000 00 0 0 000 10000 111011110100000011111011 0 01001From Binary Decision Trees to DiagramsAn Ordered Binary Decision Diagram (OBDD) is an ordered decision tree where• All isomorphic subtrees are combined, and• All nodes with isomorphic children are eliminated.Given a parameter ordering, OBDD is unique up to isomorphism.• R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEETransactions on Computers, C-35(8):677–691, 1986.OBDD for Comparator ExampleIf we use the ordering a1< b1< a2< b2for the comparator function, we obtain theOBDD below:00001111b1a1b1a2b2b2101001Variable Ordering ProblemThe size of an OBDD depends critically on the variable ordering.If we use the ordering a1< a2< b1< b2for the comparator function, we get theOBDD below:a1a2b ba2b b1 1 1 1bb22100111000101110010110a2a1Variable Ordering Problem (Cont.)For an n-bit comparator:• if we use the ordering a1< b1< . . . < an< bn, the number of vertices will be3n + 2.• if we use the ordering a1< . . . < an< b1. . . < bn, the number of vertices is3 · 2n− 1.Moreover, there are boolean functions that have exponential size OBDDs for anyvariable ordering.An example is the middle output (nthoutput) of a combinational circuit to multiplytwo n bit integers.Logical operations on OBDD’s• Logical negation: ¬f(a, b, c, d)Replace each leaf by its negation• Logicalconjunction: f(a, b, c, d) ∧ g(a, b, c, d)– UseShannon’s expansion as follows,f · g = ¯a · (f|¯a· g|¯a) + a · (f|a· g|a)to break problem intotwo subproblems. Solve subproblems recursively.– Always combine isomorphic subtrees and eliminate redundant nodes.– Hash table stores previously computed subproblems– Number of subproblems bounded by |f| · |g| .Logical operations (cont.)• Boolean quantification: ∃a : f (a, b, c, d)– By definition,∃a : f = f |¯a∨ f|a– f(a, b, c, d)|¯a: replace all a nodes by left sub-tree.– f(a, b, c, d)|a: replace all a nodes by right sub-tree.Using the above operations, we can build up OBDD’s for complex boolean functionsfrom simpler


View Full Document
Download lecture
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view lecture and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view lecture 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?