Bounded Model Checking

50 %
50 %
Information about Bounded Model Checking
Entertainment

Published on January 16, 2008

Author: Bernardo

Source: authorstream.com

Bounded Model Checking:  Bounded Model Checking Presented by Wenkai Tan Nov 5, 2002 Why we need Model Checking?:  Why we need Model Checking? The obstacle to “help computers help us more” – Design Validation Simulation and testing Formal verification 1. Deductive verification 2. Model checking What is Model Checking?:  What is Model Checking? Exhaustively traverses all the reachable states of the system to verify the desired properties + Fully automatic + Gives a counterexample when the desired property is not satisfied - Can only check finite state system - State explosion The history of Model Checking:  The history of Model Checking Explicit representation Model Checking -- very small state space, ~220 BDD based Symbolic Model Checking -- 10120, but still not enough Bounded Model Checking with satisfiability solving -- very efficient in safety and liveness properties so far Explicit representation Model Checking:  Explicit representation Model Checking Use a Kripke structure M = (S, S0, R, L) to represent the system and temporal logic to describe the desired properties Temporal logic AGp AFP BDDs and Symbolic Model Checking:  BDDs and Symbolic Model Checking 1. BDDs are directed, acyclic graphs that hold a compressed form of truth table of a Boolean function 2. BDDs share sub-terms of the function to obtain the compression 3. BDDs are very sensitive to orderings of variables and finding a good ordering is NP-Complete An example for OBDD:  An example for OBDD Binary decision tree for the two-bit comparator, f (a1,a2,b1,b2) = (a1↔b1) ∧ (a2↔b2) a1 0 1 b1 a2 a2 0 1 b2 b2 0 1 b2 b2 0 1 0 1 1 0 0 1 0 1 0 1 0 1 0 0 0 0 b1 a2 a2 0 1 b2 b2 0 1 b2 b2 0 1 0 1 0 0 0 1 0 1 0 1 0 0 1 0 0 1 An example for OBDD:  An example for OBDD a1 b1 a2 0 1 0 b2 0 0 1 b1 1 b2 0 0 1 0 1 1 1 a1 a2 a2 0 1 b1 b1 0 1 b1 b1 0 1 b2 b2 1 0 0 1 0 1 1 0 0 1 1 0 0 1 OBDDs and Symbolic Model Checking:  OBDDs and Symbolic Model Checking 1. The reachable state-space is represented by a OBDD 2. The property is evaluated recursively, by iterative fix point computations on the reachable state-space 3. The size of the OBDD is typically the bottle-neck of Model Checking Bounded Model Checking:  Bounded Model Checking In bounded model checking, we construct a Boolean formula that is satisfiable iff the underlying state transition system can realize a finite sequence of state transitions that reaches certain states of interest. Bounded Model Checking:  Bounded Model Checking Bounded model checking based on SAT procedures not BDD, hence 1. Smart DFS search of SAT potentially will get faster to a satisfying sequence (counterexample) 2. No exponential space Propositional formula of bounded model checking:  Propositional formula of bounded model checking Given: -- a transition system, M, -- a temporal logic formula, f and -- a user supplied bound, k The unrolled transition relation is [[ M ]]k := I (s0)∧ Propositional formula of bounded model checking:  Propositional formula of bounded model checking Example: Consider the CTL formula, EFp. We wish to check whether it can be verified in two time steps, i.e., k=2 [[ M, f ]]2 := I (s0)∧T (s0, s1)∧T (s1,s2)∧ ( p (s0)∨ p (s1)∨p (s2) ) Example I:  Example I 2-bit counter Safety Property:  Safety Property Is there a state reachable within k cycles, which satisfies (l∧r) to get counter example. I (s0) : ( ¬l0∧¬r0 ) ∧ T (s0, s1) : ((l1↔l0 r0)∧(r1↔ ¬r0)) ∧ T (s1, s2) : ((l2↔l1 r1)∧(r2↔ ¬r1)) ∧ p (s0) : (l0 ∧ r0 ∨ p (s1) : l1 ∧ r1 ∨ p (s2) : l2 ∧ r2 ) p = AG (¬ l ∨ ¬ r). k = 2 Example II:  Example II Liveness Property:  Liveness Property First let inc (s,s’) = (l’↔l r )∧(r’↔¬r). So, T (s,s’) = inc (s,s’)∨(l∧¬r∧l’∧¬r’) We check the satisfiability of EG(¬l∨¬r) to get counter example for p First, s0, s1, s2 must be part of valid path starting from the initial state Second, the sequence of s0, s1, s2 must be part of a loop p = AF (l ∧ r). k = 2 Liveness Property:  Liveness Property I (s0) : ( ¬l0∧¬r0 ) ∧ T (s0, s1) : ((l1↔l0 r0)∧(r1↔ ¬r0) ∨ l1∧¬r1∧ l0∧¬r0 ) ∧ T (s1, s2) : ((l2↔l1 r1)∧(r2↔ ¬r1) ∨ l2∧¬r2∧ l1∧¬r1) ) ∧ T (s2, s3) : ((l3↔l2 r2)∧(r3↔ ¬r2) ∨ l3∧¬r3∧ l2∧¬r2) ) ∧ s3 = s0 : ( (l3↔l0)∧(r3↔r0) ∨ s3 = s1 : (l3↔l1)∧(r3↔r1) ∨ s3 = s2 : (l3↔l0)∧(r3↔r0) ) ∧ p (s0) : ( ¬l0 ∨ ¬r0 ) ∧ p (s1) : ( ¬l1 ∨ ¬r1 ) ∧ p (s2) : ( ¬l2 ∨ ¬r2 ) BMC:  BMC At CMU, a model checker called BMC has been implemented, based on bounded model checking. It’s input language is a subset of the SMV language. It takes in a circuit description, a property to be proven, and a user supplied time bound k. It then generates the propositional formula. Experimental Results:  Experimental Results 1. We investigate a sequential shift and add multiplier. We specify that when the sequential multiplier is finished, its output is the same as the output of a certain combinational multiplier. Experimental Results:  Experimental Results 2. An asynchronous circuit for distributed mutual exclusion. It consists of n cells and n users. We proved the liveness property that a request for using the resource will eventually be acknowledged. We also add the fairness constraint that each asynchronous gate does not delay execution. Experimental Results:  Experimental Results 3. Repeated the experiment 2 with a buggy design, by removing several fairness constraints. Experiments on Industrial Design:  Experiments on Industrial Design Experiments on subcircuits from a PowerPC microprocessor of Motorola. To check 20 assertions. First turn each assertion into an AGp property. For each of the properties, 1. Check whether p is a tautology. 2. Check whether p is otherwise an invariant. 3. Check whether AGp hold for various time bounds ,k, from 0 to 20. Experiments on Industrial Design:  Experiments on Industrial Design 1. For combinational tautology checking we eliminate all initialization statements and run BMC with a bound of k =0. Under these conditions, the specification could hold only if p was true for all assignments to its state variables. Experiments on Industrial Design:  Experiments on Industrial Design 2. Invariance checking entails checking whether the formula holds in all initial states and is preserved by the transition relation. So, first run BMC with all initialization assignments with a time bound of k=0. Then remove all initialization assignments and add initial states predicate, run BMC with a time bound of k=1. Experiments on Industrial Design:  Experiments on Industrial Design AGp not holding under these conditions could possibly be due to behaviors in unreachable states. For instance, if an unreachable state s, existed which satisfied p but had a successor s’, which did not, then the check will fail. So, this technique can show that p is an invariant, but can’t show that it is not. Experiments on Industrial Design:  Experiments on Industrial Design As a comparison, the results of BDD-based model checking are that SMV was given each of the 20 properties separately, but completed only one of these verifications Verification Methodology:  Verification Methodology 1. Annotate each design block with Boolean formulae required to hold at all time points. Call these the block’s inner assertions. 2. Annotate each design block with Boolean formulae describing constraints on that block’s inputs. Call these the block’s input constraints. 3. check each block’s inner assertions under its input constraints, using bounded model checking with satisfiability solving. Incorporating Constraints:  Incorporating Constraints 1. Formula (1) without constraints [[ M ]]k := I (s0)∧ (1) 2. Formula (2) with constraints [[ M ]]k := I (s0)∧c (s0)∧T (s0,s1)∧c (s1) ∧…∧T (sk-1,sk)∧c (sk) (2) Safety Property Checking Procedure:  Safety Property Checking Procedure 1. Check whether p is a combinational tautology in the unconstrained K, using formula 1. If it is, exit. 2. Check whether p is an inductive invariant for the unconstrained K, using formula 1. If it is, exit. 3. Check whether p is a combinational tautology in the presence of input constraints, using formula 2. If it is, go to step 6. 4. Check whether p is an inductive invariant in the presence of input constraints, using formula 2. It it is, go to step 6. Safety Property Checking Procedure:  Safety Property Checking Procedure 5. Check if a bounded length counterexample exists to AGp in the presence of input constraints, using formula 2. If one is found, there is no need to examine c, since the counterexample would exist without input constraints. If a counterexample is not found, go to step 6. The input constraints may need to be reformulated and this procedure repeated from step 3. Safety Property Checking Procedure:  Safety Property Checking Procedure 6. Check the input constraints, c. Inputs that are constrained in one design block, A, will, in general, be outputs of another design block, B. We turn them into inner assertions for B, and check them with the above procedure. Also circular reasoning can be deleted automatically. Conclusions:  Conclusions + Entails only slight memory and CPU usage. + Extremely fast for invariance checking. + Counterexamples and witnesses are of minimal length, which make them easy to understand. + Well to automation, needs little by-hand intervention. - Implementations are limited as to the types of properties that can be checked - No clear evidence that the technique will consistently find long counterexample or witnesses. Directions for future research:  Directions for future research 1. The use of domain knowledge to guide search in SAT procedures. 2. New technique for approaching completeness, especially in safety property checking, where it may be the most possible. 3. Combining bounded model checking with other reduction techniques 4. Combining bounded model checking with partial BDD approach.

Add a comment

Related presentations

Related pages

Model checking - Wikipedia

Bounded model checking algorithms unroll the FSM for a fixed number of ... SMART Model checker, Symbolic Model checking Analyzer for Reliability and Timing;
Read more

Bounded Model Checking Using Satisfiability Solving

Bounded Model Checking Using Satisfiability Solving? Edmund Clarke1, Armin Biere2, Richard Raimi3, and Yunshan Zhu4 1 Computer Science Department, CMU ...
Read more

CBMC Bounded Model Checking software - cprover.org

CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99, most of C11 and most compiler extensions provided by gcc and Visual Studio.
Read more

Bounded Model Checking - John Franco

“p02c00˙bmc” — 2008/11/20 — 10:13 — page 459 — #5 Chapter 14. Bounded Model Checking 459 temporal operators are the “next time ...
Read more

Concurrent Bounded Model Checking - ti.arc.nasa.gov

Concurrent Bounded Model Checking Quoc-Sang Phan 1, Pasquale Malacaria , and Corina S. P as areanu2 1 Queen Mary University of London 2 Carnegie Mellon ...
Read more

Symbolic Bounded Model Checking of Abstract State Machines

Margus Veanes, et al.: Symbolic bounded model checking of abstract state machines 151 E:= E - {(v,w) | w in V} V:= V - {v} This model program specifles ...
Read more

Bounded Model Checking - JKU

Bounded Model Checking Armin Biere1 Alessandro Cimatti2 Edmund M. Clarke3 Ofer Strichman3 Yunshan Zhu4 ? 1 Institute of Computer Systems, ETH Zurich, 8092 ...
Read more

Bounded Model Checking (BMC)

Background: model checking a finite transition system M a property P (in some temporal logic) Given: The model checking problem:
Read more

CBMC: Bounded Model Checking for ANSI-C

Bounded Model Checking I Bounded Model Checking (BMC) is the most successful formal validation technique in the hardware industry I Advantages: 4 Fully ...
Read more

LLBMC: Bounded Model Checking KLEE: Symbolic Execution

Inhalt 1 17. Juni 2013 S. Falke - LLBMC und KLEE ITI KIT 1.Einführung 2.Bounded Model Checking mit LLBMC 3.Symbolic Execution mit KLEE
Read more