资源描述：
《bounded model checking (bmc-08)》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、Bounded Model Checking (BMC)Dr Olga TveretinaSummer semester, 2009Background: model checkingGiven:a finite transition systemMa property P (in some temporal logic)The model checking problem: Does P holds in M??M
2、= PTemporal propertiesSafetyproperties:“
3、Always x=y”G (x=y)Liveness properties: “Reset can always be reached”GF Reset “From some point on, always switch_on”FG switch_onOBDDs and symbolic model checkingOBDD is a canonical form to represent Boolean functionsThey are often more compact than '
4、traditional' normal forms as CNFs, DNFs and can be manipulated efficientlyThe reachable statespace is represented by a OBDDThe property is evaluated recursively, by iterative fix point computations on the reachable statespaceProblems with OBDDsBDDs are
5、 a canonical representation, but often become too largeVariable ordering must be uniformalong paths.Selecting right variable ordering very important to built small BDDstime consuming or needs manual interventionin some cases no space efficient variabl
6、e ordering existsAlternative approaches to model checking use SAT proceduresAdvantages of SAT proceduresSAT procedures also operate on Boolean formulas but do not use canonical formsDo not suffer from the potential space explosion of BDDsDifferent ord
7、erings of variables are possible on different branchesThere exist very efficient implementationsSAT solver progress 1960 2010(E.Clarke)100000100001000Vars100101196019701980199020002010YearBounded model checkingA. Biere, A. Cimatti, E. Clarke, Y. Zhu, S
8、ymbolic Model Checking without BDDs, TACAS’99E. Clarke, A. Biere, R. Raimi, Y. Zhu, Bounded Model Checking Using Satisfiability Solving, 2001Bounded model checkingBased on SATThere is a counterexample of length k <=> pro
9、positional formula is satisfiableBMC for LTL reduced to SAT in poly timeExample:Most of the safety properties can be expressed as 'always p', where p is a propositional variableIs there a state reachable within k steps that satisfies ¬p
