Bounded Model Checking

Information about Bounded Model Checking

Published on January 16, 2008

Author: Bernardo

Source: authorstream.com

Content

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.

Related presentations


Other presentations created by Bernardo

expert diabetes
07. 02. 2008
0 views

expert diabetes

Indus Valley Civilization
17. 01. 2008
0 views

Indus Valley Civilization

1976 election
09. 01. 2008
0 views

1976 election

kitchen safety
10. 01. 2008
0 views

kitchen safety

07 cover
11. 01. 2008
0 views

07 cover

BPP Period 6
12. 01. 2008
0 views

BPP Period 6

ira
15. 01. 2008
0 views

ira

CVD for CHAT1
17. 01. 2008
0 views

CVD for CHAT1

siriexcavation
18. 01. 2008
0 views

siriexcavation

u13l4abolitionppt
19. 01. 2008
0 views

u13l4abolitionppt

ge390 ch2 origins cities
20. 01. 2008
0 views

ge390 ch2 origins cities

Workplace Safety
20. 01. 2008
0 views

Workplace Safety

best advpromo
23. 01. 2008
0 views

best advpromo

The Meaning of Sports
24. 01. 2008
0 views

The Meaning of Sports

J2ME
04. 02. 2008
0 views

J2ME

Technology
04. 02. 2008
0 views

Technology

BNAIC04
05. 02. 2008
0 views

BNAIC04

Euram07 B Bourigeaud
25. 01. 2008
0 views

Euram07 B Bourigeaud

Module 5 Lead respirators
18. 01. 2008
0 views

Module 5 Lead respirators

Guncotton
28. 01. 2008
0 views

Guncotton

39 Isaiah 50 53
29. 01. 2008
0 views

39 Isaiah 50 53

FoodChildSafetyTrain ing
04. 02. 2008
0 views

FoodChildSafetyTrain ing

Basic Nutrition
06. 02. 2008
0 views

Basic Nutrition

piano
07. 02. 2008
0 views

piano

DEC Presentation
07. 02. 2008
0 views

DEC Presentation

the noble gases
15. 02. 2008
0 views

the noble gases

Localized
18. 02. 2008
0 views

Localized

Sunday Randa SAADEH Revit BFHI
15. 01. 2008
0 views

Sunday Randa SAADEH Revit BFHI

schizo franck7
28. 01. 2008
0 views

schizo franck7

Weather Patterns and Forecasts
27. 02. 2008
0 views

Weather Patterns and Forecasts

act schol pol
11. 01. 2008
0 views

act schol pol

durerHis
03. 03. 2008
0 views

durerHis

presentation on budget process
07. 03. 2008
0 views

presentation on budget process

The temple mount
10. 03. 2008
0 views

The temple mount

Finregul 13
05. 03. 2008
0 views

Finregul 13

Disney1
19. 03. 2008
0 views

Disney1

A1 Introduction
20. 03. 2008
0 views

A1 Introduction

Judy Kersey SWE ECEDHA
14. 02. 2008
0 views

Judy Kersey SWE ECEDHA

Reed Final Dengue
03. 04. 2008
0 views

Reed Final Dengue

LatinAmericaHistoryp pt
07. 04. 2008
0 views

LatinAmericaHistoryp pt

taking the gamble
27. 03. 2008
0 views

taking the gamble

SC25 WG1 N1208
08. 04. 2008
0 views

SC25 WG1 N1208

sportdiscus
17. 04. 2008
0 views

sportdiscus

The Bahai Faith
15. 01. 2008
0 views

The Bahai Faith

STILWELL2001
18. 04. 2008
0 views

STILWELL2001

DVC Powerpoint May14
21. 04. 2008
0 views

DVC Powerpoint May14

2286
22. 04. 2008
0 views

2286

cbnen6a
24. 04. 2008
0 views

cbnen6a

Leg PowerPoint
14. 01. 2008
0 views

Leg PowerPoint

MLA SCASL 06
25. 02. 2008
0 views

MLA SCASL 06

2 3 IVARSSON PPT
07. 05. 2008
0 views

2 3 IVARSSON PPT

DomainStalking
08. 05. 2008
0 views

DomainStalking

hart
30. 04. 2008
0 views

hart

DVC9804
19. 03. 2008
0 views

DVC9804

How Societies Remember
02. 05. 2008
0 views

How Societies Remember

nfarlee
29. 02. 2008
0 views

nfarlee

23 TheFringe alt
22. 01. 2008
0 views

23 TheFringe alt

Dada
15. 01. 2008
0 views

Dada

ah experiences
22. 01. 2008
0 views

ah experiences

Lab3 2006
16. 01. 2008
0 views

Lab3 2006

zACS mtg 4 16 97
28. 01. 2008
0 views

zACS mtg 4 16 97

Folk Art
10. 01. 2008
0 views

Folk Art

corporatepartnership
23. 01. 2008
0 views

corporatepartnership

Giamarchi
10. 01. 2008
0 views

Giamarchi

2002 Vocabulary
31. 03. 2008
0 views

2002 Vocabulary

20080120 1
04. 02. 2008
0 views

20080120 1