PowerPoint PresentationUseful LinksSMV: Symbolic Model VerifierLanguage CharacteristicsA Sample SMV ProgramVariable AssignmentsSpecificationsASSIGN and DEFINEMore on Case StatementNondeterminismModules and HierarchyModules and Hierarchy - ExampleModule CompositionAsynchronous CompositionCounterexamplesFairnessCounter RevisitedModeling Shared VariablesImplicit ModelingImplicit Modeling ExampleTRANSShared Data Example - main moduleShared Data Example - user module 1Shared Data Example - user module 2Guarded CommandsGuarded Commands PitfallTRANS GuidelinesSMV StepsSynchronous vs. AsynchronousRun SMVSMV OptionsSMV Options: Variable orderingSMV Options: Transition relationMutual Exclusion -1Mutual Exclusion -2Mutual Exclusion: CounterexampleLecture 9: SMV: An IntroductionBased on lectures by Dong Wang and Marius Minea.2Useful LinksCMU Model checking homepagehttp://www.cs.cmu.edu/~modelcheck/SMV windows versionhttp://www.cs.cmu.edu/~modelcheck/smv.html#ntSMV man page (must read)http://www.cs.cmu.edu/~dongw/smv.txtSMV manualhttp://www.cs.cmu.edu/~modelcheck/smv/smvmanual.ps3SMV: Symbolic Model VerifierKen McMillan, Symbolic Model Checking: An Approach to State Explosion Problem, 1993.Finite-state Systems described in a specialized languageSpecifications given as CTL formulasInternal representation using BDDsAutomatically verifies specification or produce counterexamples4Language CharacteristicsAllows description of synchronous and asynchronous systemsModularized and hierarchical descriptionsFinite data types: boolean, enum, int etcNondeterminismVariety of specifications: safety, liveness, deadlock freedom5A Sample SMV ProgramMODULE mainVAR request: boolean; state: {ready, busy};ASSIGN init(state) := ready; next(state) := case state=ready & request: busy; 1: {ready, busy}; esac;SPEC AG(request  AF (state = busy))6Variable AssignmentsAssignment to initial state: init(value) := 0;Assignment to next state: transition relation next(value) := value + carry_in mod 2;Assignment to current state: invariant relationcarry_out := value & carry_in;SMV is a parallel assignment language7SpecificationsEF p : from all initial states, a state where p holds is reachable.A[p U q] : p remains true until q is true.AG AF p : p is true infinitely often on very compution path.AG (req  AF ack) : any request will be eventually acknowledged.8ASSIGN and DEFINEVAR a: boolean;ASSIGN a := b | c;•declares a new state variable a•becomes part of invariant relationDEFINE d:= b | c;•is effectively 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 d9More on Case StatementCase statement is converted to if-then-else internally, so all the guards are evaluated sequentially.If none of the guards are true, an arbitrary valid value is returned.10NondeterminismCompletely unassigned variable can model unconstrained input.{val_1, …, val_n} is an expression taking on any of the given values nondeterministically.Nondeterministic choice•to model an implementation that has not been refined yet•In abstract models where a value of some state variable cannot be completely determined11Modules and HierarchyModules can be instantiated.Each program has a module mainScoping•Variables declared outside a module can be passed as parameters.•Internal variables of a module can be used in enclosing modules(submodel.varname). Parameters are passed by reference.12Modules and Hierarchy - ExampleMODULE mainVAR bit0 : counter_cell(1);bit1 : counter_cell(bit0.carry_out); bit2 : counter_cell(bit1.carry_out);SPEC AG AF bit2.carry_outMODULE counter_cell(carry_in)VAR value : boolean;ASSIGN init(value) := 0; next(value) := value + carry_in mod 2;DEFINE carry_out := value & carry_in;13Module CompositionSynchronous composition•All assignments are executed in parallel and synchronously.•A single step of the resulting model corresponds to a step in each of the components.Asynchronous composition•A step of the composition is a step by exactly one process.•Variables, not assigned in that process, are left unchanged.14Asynchronous CompositionMODULE mainVAR gate1: process inverter(gate3.output);gate2: process inverter(gate1.output);gate3: process inverter(gate2.output);SPEC (AG AF gate1.output)SPEC (AG AF !gate1.output)MODULE inverter(input)VAR output: boolean;ASSIGN init(output) := 0; next(output) := !input;15Counterexamples-- specification AG AF (!gate1.output) is false-- as demonstrated by the following executionstate 2.1:gate1.output = 0 gate2.output = 0 gate3.output = 0state 2.2:[executing process gate1]-- loop starts here --state 2.3:gate1.output = 1[stuttering]state 2.4:[stuttering]16FairnessFairness constraint•FAIRNESS ctl_formulae•Assumed to be true infinitely often•Model checker only explores paths satisfying fairness constraintFAIRNESS running17Counter RevisitedMODULE mainVARcount_enable: boolean;bit0 : counter_cell(count_enable);bit1 : counter_cell(bit0.carry_out); bit2 : counter_cell(bit1.carry_out);SPEC AG AF bit2.carry_outFAIRNESS count_enable18Modeling Shared VariablesMODULE zero(a)ASSIGN next(a) := 0;FAIRNESS runningMODULE one(b)ASSIGN next(b) := 1;FAIRNESS runningMODULE mainVAR x: boolean; z: process zero(x); o: process one(x);SPEC AG AF (x = 0)19Implicit ModelingINIT boolean_expr•Initial states will be those satisfy boolean_expr.•There is no next operator in boolean_expr.INVAR boolean_expr•The set of states is restricted to those satisfy boolean_expr•There is no next operator in boolean_expr.TRANS boolean_expr•Restrict the transition relation.20Implicit Modeling ExampleINVAR (!enable -> stutter)TRANS ((state = idle & next(state) = request) | (state = request & sema & turn = id & (next(state) = critical & next(sema) = 0) | (state = critical & next(state) = release))21TRANSAdvantages•Group assignments to different variables•Good for modeling guarded commandsDisadvantages - easy to make mistakes•Contradictory constraints-Transition relation is empty, reachable states is 0.-Transition relation is not total.•Missing cases22Shared Data Example - main moduleTwo users assign pid to shared data in turnMODULE mainVAR data: boolean; turn: boolean; user0: user(0, data, turn); user1: user(1, data, !turn);ASSIGNnext(turn) := !turn;SPEC AG (AF data & AF (!data))23Shared Data Example - user module 1Using ASSIGN and case statement won’t