形式验证简介-计算机科学国家重点实验室.ppt

1、1,Model Checking,E. M. Clarke, O. Grumberg, D. A. Peled,2,Model Checking,Models,Temporal Logics,Model CheckingKripke StructureGraph (SCC)TableauxAutomata Symbolic (BDD, Fixpoint)On the FlyPartial order reduction,3,Chapter 2: Modeling Systems,Modeling Concurrent SystemsKripke Structure (S,S0,R,L)Firs

2、t Order Representation (V,S0,R)Granularity of TransitionsConcurrent SystemsDigital Circuits (Synchronous/Asynchronous)ProgramsConcurrent Programs,4,Chapter 3: Temporal Logics,CTL*Temporal OperatorsPath QuantifierPath and State FormulasCTL and LTLCTL/ACTLLTLFairnessFairness ConstraintsFair Kripke Str

3、ucture (S,R,L,F)Fair Semantics,5,Chapter 4: Model Checking,CTL Model Checking (Labeling)CheckEU CheckEGFairness (CheckFairEG)LTL Model Checking by TableauPSPACE/NP-HardTableau Construction (s,K)Check Self-fulfilling SCCCTL* Model CheckingCTL and LTL SubformulasDivide and Conquer,6,Chapter 5: Binary

4、Decision Diagrams,Representing Boolean Formulas/FunctionsOrdered Binary Decision TreesOrdered Binary Decision DiagramsOBDD OperationsRepresenting Kripke StructureBoolean Representation of VariablesRelation = Characterization FunctionCharacterization Function = OBDD(S,S0,R,L) = OBDDs,7,Chapter 6: Sym

5、bolic MC,Fixpoint RepresentationFixpointFixpoint ComputationCTL FormulasSymbolic CTL Model CheckingQuantifier Boolean FormulasCheckEX/CheckEU/CheckEGFairnessFixpoint Representation of Fair EGf CheckFairEG/CheckFairEX/CheckFairEU,8,Chapter 6(2): Symbolic MC,Counterexamples and WitnessesRelational Pro

6、duct ComputationRelProdPartitioned Transition Relations Symbolic LTL Model CheckingTableaux for LTL FormulasProduct of Kripke Structures and LTL TableauxFairness Constraints for Until-SubformulasSymbolic Model Checking,9,Chapter 7: MC for -Calculus,Propositional -CalculusModified Kripke Structure (S

7、,T,L)Relational Variables and EnvironmentsAlternation DepthEvaluating Fixpoint FormulasAlgorithmsOBDD RepresentationCTL to -CalculusComplexity,10,Chapter 9: MC and Automata,Automata Finite WordsInfinite WordsBuchi AutomataNondeterministic Buchi AutomataGeneralized Buchi AutomataChecking EmptinessDou

8、ble DFSCorrectness,11,Chapter 9(2): MC and Automata,LTL to AutomataOn the Fly Model CheckingChecking Language Containment Symbolically,12,Chapter 10: Partial Order Reduction,Concurrency in Asynchronous SystemsDepth First Search ample(s) versus enabled(s)Independence and InvisibilityIndependenceInvis

9、ibilityInvariant under Stuttering Partial Order Reduction for LTL_xc0 c4,13,Chapter 10(2): Partial Order Red.,Calculating Ample Setsc0, c2, c1 Heuristic, c3 c3HeuristicOn the Fly ReductionCorrectnessPartial Order Reduction in SPINMC in Practice,14,Chapter 8: MC in Practice,SMV Model CheckerModules S

10、ynchronous and interleaved CompositionNondeterministic TransitionsTransition RelationsModel Checking Example IEEE Futurebus+ Standard,15,归类,不同类型的模型不同类型的时序逻辑各种模型检测算法(优化方法)及算法正确性分析模型检测工具和实例,16,模型,Kripke StructuresFair Kripke StructuresModified Kripke StructuresFirst Order RepresentationDigital Circuit

11、s (Synchronous/Asynchronous)Programs and Concurrent ProgramsBuchi AutomataGeneralized Buchi Automata,模型之间的关系,模型之间的转换,不同模型的特点,17,时序逻辑,CTL*CTL/ACTLLTL-Calculus,逻辑的语法语义,不同逻辑的关系,不同逻辑的特点,18,模型检测相关算法(1),CTL Model Checking (Labeling)LTL Model Checking by TableauCTL* Model CheckingSymbolic CTL Model Checkin

12、gSymbolic Fair CTL Model CheckingSymbolic LTL Model CheckingModel Checking for -CalculusChecking Emptiness,算法复杂性,算法的基本原理,算法正确性,19,模型检测相关算法(2),Counterexamples and WitnessesRelational Product ComputationLTL to AutomataCTL to -CalculusConcurrent Programs to First Order Rep.,20,模型检测相关算法(3),On the Fly Mo

13、del CheckingPartial Order ReductionHeuristics for Ample SetsChecking Language Containment Symbolically,21,模型检测算法相关数据结构,OBDD,表示方法,化简和计算方法,22,模型检测工具,SMV IEEE Futurebus+ StandardSPIN Leader Election,总体课程目标,掌握模型检测基础理论不同类型的模型不同类型的时序逻辑各种模型检测算法及算法正确性分析具备模型检测方法研究及应用的能力能够较快阅读本专业方向的文献能够针对特定问题设计模型检测算法能够应用模型检测方法和工具对特定问题进行验证,