Unformatted text preview:

© 2011 Carnegie Mellon University Introduction to SMV Part 2 Arie Gurfinkel (SEI/CMU) based on material by Prof. Clarke and others© 2011 Carnegie Mellon University Brief Review3 © 2011 Carnegie Mellon University 2/18/2005!3 Symbolic Model Verifier (SMV) Ken McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem, 1993. Finite-state Systems described in a specialized language Specifications given as CTL formulas Internal representation using ROBDDs Automatically verifies specification or produces a counterexample4 © 2011 Carnegie Mellon University 2/18/2005!4 A Sample SMV Program (short.smv) MODULE!main!VAR*!!!!!request:!boolean;!!!!!!state:!{ready,!busy};!ASSIGN*!!!!!init(state)!:=!ready;!!!!!!next(state)!:=!!!case!!!!state=ready!&!request:!busy;!!!!TRUE !:!{ready,!busy};!!esac;!SPEC!AG(request!B>!AF!(state!=!busy))!5 © 2011 Carnegie Mellon University A Three-Bit Counter MODULE!main!VAR!!!bit0!:!counter_cell(TRUE);!!!bit1!:!counter_cell(bit0.carry_out);!!!bit2!:!counter_cell(bit1.carry_out);!*SPEC**AG*AF*bit2.carry_out*!MODULE!counter_cell(carry_in)!VAR!!!value!:!boolean;!ASSIGN!!!init(value)!:=!FALSE;!!!next(value)!:=!value!xor!carry_in;!DEFINE!!!carry_out!:=!value!&!carry_in;!value!+!carry_in!mod!2!6 © 2011 Carnegie Mellon University in out val in out in out in out val val val module instantiations bit0 bit1 bit2 module declaration7 © 2011 Carnegie Mellon University Inverter Ring MODULE!main!VAR!!!gate1!:!process!inverter(gate3.output);!!!gate2!:!process!inverter(gate1.output);!!!gate3!:!process!inverter(gate2.output);!*SPEC!(AG*AF*gate1.output)*&*(AG*AF*!gate1.output)*!MODULE!inverter(input)!VAR!!!output!:!boolean;!ASSIGN!!!init(output)!:=!FALSE;!!!next(output)!:=!!input;!!FAIRNESS!!!running!8 © 2011 Carnegie Mellon University Fairness • Assumed to be true infinitely often • Model checker only explores paths satisfying fairness constraint • Each fairness constraint must be true infinitely often If there are no fair paths • All existential formulas are false • All universal formulas are true FAIRNESS*Ctlform!FAIRNESS*running!9 © 2011 Carnegie Mellon University Can A TRUE Result of Model Checker be Trusted Antecedent Failure [Beatty & Bryant 1994] • A temporal formula AG (p ⇒ q) suffers an antecedent failure in model M iff M ⊧ AG (p ⇒ q) AND M ⊧ AG (¬p) Vacuity [Beer et al. 1997] • A temporal formula ϕ is satisfied vacuously by M iff there exists a sub-formula p of ϕ such that M ⊧ ϕ[p←q] for every other formula q • e.g., M ⊧ AG (r ⇒ AF a) and M ⊧ AG (r ⇒ AF ¬a) and AG (r ⇒ AF ¬r) and AG (r ⇒ AF FALSE), …10 © 2011 Carnegie Mellon University Vacuity Detection: Single Occurrence ϕ is vacuous in M iff there exists an occurrence of a subformula p such that • M ⊧ ϕ[p ← TRUE] and M ⊧ ϕ[p ← FALSE] M ⊧ AG (req ⇒ AF TRUE) M ⊧ AG TRUE M ⊧ AG (req ⇒ AF FALSE) M ⊧ AG ¬req M ⊧ AG (TRUE ⇒ AF ack) M ⊧ AG AF ack M ⊧ AG (FALSE ⇒ AF ack) M ⊧ AG TRUE11 © 2011 Carnegie Mellon University Detecting Vacuity in Multiple Occurrences: ACTL An ACTL ϕ is vacuous in M iff there exists an a subformula p such that • M ⊧ ϕ[p ← x] , where x is a non-deterministic variable Is AG (req ⇒ AF req) vacuous? Should it be? Is AG (req ⇒ AX req) vacuous? Should it be? Always vacuous!!! M ⊧ AG (x ⇒ AF x) M ⊧ AG TRUE Can be vacuous!!! M ⊧ AG (x ⇒ AX x) can’t reduce12 © 2011 Carnegie Mellon University Run NuSMV NuSMV![options]!inputfile!• Bint! !interactive!mode!• Blp! !list!all!properties!• Bn!X! !check!property!number!X!• Bctt !check!totality!of!transition!relation!• Bold !compatibility!mode!• Bofm!file!output!flattened!model ! !!13 © 2011 Carnegie Mellon University Using NuSMV in Interactive Mode Basic Usage • go!– prepare model for verification • check_ctlspec!– verify properties Simulation • pick_state![Bi]![Br]!– pick initial state for simulation [interactively] or [randomly] • simulate![Bi]![r]!s!– simulate the model for ‘s’ steps [interactively] or [randomly] • show_traces!– show active traces14 © 2011 Carnegie Mellon University Useful Links NuSMV home page • http://nusmv.fbk.eu/ NuSMV tutorial • http://nusmv.fbk.eu/NuSMV/tutorial/v25/tutorial.pdf NuSMV user manual • http://nusmv.fbk.eu/NuSMV/userman/v25/nusmv.pdf NuSMV FAQ • http://nusmv.fbk.eu/faq.html NuSMV on Andrew • /afs/andrew.cmu.edu/usr6/soonhok/public/NuSMV-zchaff-2.5.3-x86_64-redhat-linux-gnu/ NuSMV examples • <NuSMV>/share/nusmv/examples Ken McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem, 1993 • http://www.kenmcmil.com/pubs/thesis.pdf15 © 2011 Carnegie Mellon University Today: 3 Examples Mutual Exclusion Bus Protocol Traffic Light Controller16 © 2011 Carnegie Mellon University Example 1: Mutual Exclusion Two processes want access to a shared resource • they go through idle, trying, critical states Safety (Mutual Exclusion) • Only one process can be in the critical section at any given time – AG ( !(p0 = critical & p1 = critical) ) Liveness (No Starvation) • If a process is trying to enter critical section, it eventually enters it – AG (p0 = trying -> AF p0 = critical)Ed Clarke Daniel Kroening Carnegie Mellon University SMV Example: Bus ProtocolOverview Node 1 Design goals: l Collision free operation l Priorities for the nodes Preliminaries: l Single, shared bus l Every node can broadcast on this bus Node 2 Node 3 Node 4 Similar busses are used in the automotive industry l CAN l ByteflightBasic Idea Achieve design goals by: l Assign unique time to each node l Guarantees Collision free operation l The node with the lower time gets priority Operation Principle l Round based algorithm l First person to start sending gets the bus ÜExample Node 1 Node 2 Node 3 Node 4 ·- ¸ ¹ º Bus time ÂExample Node 1 Node 2 Node 3 Node 4 ·- ¸ ¹ º Bus time ·- Hm, I won’t sendExample Node 1 Node 2 Node 3 Node 4 ·- ¸ ¹ º Bus time ¸ I will send!Example Node 1 Node 2 Node 3 Node 4 ·- ¸ ¹ º Bus time ¹Example Node 1 Node 2 Node 3 Node 4 ·- ¸ ¹ º Bus time ºExample Node 1 Node 2 Node 3 Node 4 ·- ¸ ¹ º Bus time »Example Node 1


View Full Document

CMU CS 15414 - Introduction to SMV Part 2

Download Introduction to SMV Part 2
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Introduction to SMV Part 2 and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Introduction to SMV Part 2 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?