Slide 1Symbolic Model Verifier (SMV)Overview of SMVSMV VariantsNuSMV2 ArchitectureSMV LanguageA Sample SMV Program (short.smv)Slide 8A Sample SMV Program (short.smv)Slide 10SMV Syntax: ExpressionsThe Case ExpressionVariables and AssignmentsVariables and Assignments (cont’d)Circular DefinitionsNondeterminismASSIGN and DEFINESPEC DeclarationModulesPass by referencePass by referenceA Three-Bit CounterSlide 23Slide 24A Three-Bit CounterSlide 26Module CompositionInverter RingSlide 29FairnessSynchronous vs AsynchronousImplicit ModelingImplicit Modeling ExampleTRANSShared Data ExampleShared Data Example with TRANSTRANS PitfallsTRANS GuidelinesSlide 39Can A TRUE Result of Model Checker be TrustedVacuity Detection: Single OccurrenceDetecting Vacuity in Multiple OccurrencesDetecting Vacuity in Multiple Occurrences: ACTLRun NuSMVUsing NuSMV in Interactive ModeUseful Links© 2011 Carnegie Mellon UniversityIntroduction to SMVArie Gurfinkel (SEI/CMU)based on material by Prof. Clarke and others2© 2011 Carnegie Mellon University2/18/20052Symbolic Model Verifier (SMV)Ken McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem, 1993.Finite-state Systems described in a specialized languageSpecifications given as CTL formulas Internal representation using ROBDDsAutomatically verifies specification or produces a counterexample3© 2011 Carnegie Mellon University2/18/20053 Overview of SMVSMV Input LanguageFinite State Kripke StructureSpecification – CTL FormulaOBDD based Symbolic Model CheckingYesNoCounterExampleBackend4© 2011 Carnegie Mellon UniversitySMV VariantsCMUSMVCMUSMVCadenceSMVCadenceSMVNuSMVNuSMVStrong abstraction functionsGUINew languageOldest VersionNo GUITwo versions2.x: Open Source, many new features, BDD and SAT based backends1.x: Original version, had a GUI5© 2011 Carnegie Mellon UniversityNuSMV2 Architecture6© 2011 Carnegie Mellon UniversitySMV LanguageAllows description of completely synchronous to asynchronous systems, detailed to abstract systems Modularized and hierarchical descriptionsFinite data types: Boolean and enumeratedParallel-assignment syntaxNon-determinism7© 2011 Carnegie Mellon University2/18/20057A Sample SMV Program (short.smv)MODULE mainVAR request: boolean; state: {ready, busy};ASSIGN init(state) := ready; next(state) := case state=ready & request: busy; TRUE : {ready, busy};esac;SPEC AG(request -> AF (state = busy))MODULE mainVAR request: boolean; state: {ready, busy};ASSIGN init(state) := ready; next(state) := case state=ready & request: busy; TRUE : {ready, busy};esac;SPEC AG(request -> AF (state = busy))8© 2011 Carnegie Mellon University8ready!requestbusy!requestreadyrequestbusyrequestKripke structure Computation treereadyrequestbusy!requestbusyrequestholds after one stepbusyrequestholds in the initial stateAG(request -> AF (state = busy))9© 2011 Carnegie Mellon UniversityMODULE mainVAR request: boolean; state: {ready, busy};ASSIGN init(state) := ready; next(state) := casestate=ready & request: busy;TRUE : {ready, busy};esac;SPEC AG(request -> AX (state = busy))MODULE mainVAR request: boolean; state: {ready, busy};ASSIGN init(state) := ready; next(state) := casestate=ready & request: busy;TRUE : {ready, busy};esac;SPEC AG(request -> AX (state = busy))A Sample SMV Program (short.smv)2/18/20059what if AF is changed to AX ?10© 2011 Carnegie Mellon University10ready!requestbusy!requestreadyrequestbusyrequestAG(request -> AX (state = busy)) is false11© 2011 Carnegie Mellon UniversitySMV Syntax: ExpressionsExpr :: atom -- symbolic constant | number -- numeric constant | id -- variable identifier | “!” Expr -- logical not | Expr & Expr -- logical and | Expr | Expr -- logical or | Expr -> Expr -- logical implication | Expr <-> Expr -- logical equivalence | “next” “(“ id “)” -- next value | Case_expr | Set_expr12© 2011 Carnegie Mellon UniversityThe Case ExpressionCase_expr :: “case” expr_a1 “:” expr_b2 “;” … expr_an “:” expr_bn “;” “esac”Guards are evaluated sequentiallyThe first one that is true determines the resulting valueCases must be exhaustiveIt is an error if all expressions on the left hand side evaluate to FALSE13© 2011 Carnegie Mellon UniversityVariables and AssignmentsDecl :: “VAR” atom1 “:” type1 “;” atom2 “:” type2 “;” …Decl :: “ASSIGN” dest1 “:=“ Expr1 “;” dest2 “:=“ Expr2 “;” …Dest :: atom -- current | “init” “(“ atom “)” -- initial | “next” “(“ atom “)” -- next-state14© 2011 Carnegie Mellon UniversityVariables and Assignments (cont’d)State is an assignment of values to a set of state variablesType of a variable – boolean, scalar, user defined module, or array.Assignment to initial state: •init(value) := FALSE;Assignment to next state (transition relation)•next(value) := value xor carry_in;Assignment to current state (invariant)•carry_out := value & carry_in;Either init-next or invar should be used, but not bothSMV is a parallel assignment language15© 2011 Carnegie Mellon UniversityCircular Definitions… are not alloweda := next(b);next(b) := c;c := a;a := next(b);next(b) := c;c := a;init(a) := 0;next(a) := !b;init(b) := 1;next(b) := !a;init(a) := 0;next(a) := !b;init(b) := 1;next(b) := !a;16© 2011 Carnegie Mellon UniversityNondeterminismCompletely unassigned variable model unconstrained input{val_1, …, val_n} is an expression taking on any of the given values nondeterministically•next(b) := {TRUE, FALSE};Nondeterministic choice can be used to:•Model an environment that is outside of the control of the system•Model an implementation that has not been refined yet•Abstract behavior17© 2011 Carnegie Mellon UniversityASSIGN and DEFINEVAR a: boolean;ASSIGN a := b | c;•declares a new state variable a•becomes part of invariant relationDEFINE d := b | c;•a macro definition, each occurrence of d is replaced by (b | c)•no extra BDD variable is generated for d•the BDD for (b | c) becomes part of each expression using d18© 2011 Carnegie Mellon UniversitySPEC DeclarationDecl :: “SPEC” ctlformCtlform :: expr -- bool expression | “!” ctlform | Ctlform <op> Ctlform | “E” Pathform | “A” PathformPathform :: “X” Ctlform | “F”