Unformatted text preview:

Slide 1What is This All About?HistorySpin CapabilitiesSpin Overall StructurePromelaExecutabilityDelimitorsData TypesProcess DefinitionProcess InstantiationProcess ParameterizationRace ConditionDeadlockAtomic sequencesMessage passingMessage passingMessage passingMessage passingExecutabilityComposite conditionsSlide 22RendezvousExampleControl flowCase selectionSlide 27RepetitionRepetitionUnconditional jumpsProcedures and RecursionSlide 32TimeoutsAssertionsSlide 35ReferencesQuestions?© 2011 Carnegie Mellon UniversitySPIN: Part 115-414 Bug Catching: Automated Program Verification and TestingSagar ChakiOctober 31, 20112Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityWhat is This All About?Spin•On-the-fly verifier developed at Bell-labs by Gerard Holzmann and others•http://spinroot.comPromela•Modeling language for SPIN•Targeted at asynchronous systems–Switching protocols•http://spinroot.com/spin/Man/Quick.html3Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityHistoryWork leading to Spin started in 1980•First bug found on Nov 21, 1980 by Pan•One-pass verifier for safety propertiesSucceeded by•Pandora (82), •Trace (83), •SuperTrace (84), •SdlValid (88), •Spin (89)Spin covered omega-regular properties4Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversitySpin CapabilitiesInteractive simulation•For a particular path•For a random pathExhaustive verification•Generate C code for verifier•Compile the verifier and execute•Returns counter-exampleLots of options for fine-tuning5Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversitySpin Overall StructureGUIFront-endGUIFront-endPromelaParserPromelaParserLTL Parser andTranslatorLTL Parser andTranslatorSyntaxErrorReportsSyntaxErrorReportsInteractiveSimulationInteractiveSimulationVerifierGeneratorVerifierGeneratorOptimized ModelChecker (ANSI C)Optimized ModelChecker (ANSI C)Executable O-T-FVerifierExecutable O-T-FVerifierCounter ExampleCounter Example6Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityPromelaStands for Process Meta LanguageLanguage for asynchronous programs•Dynamic process creation•Processes execute asynchronously•Communicate via shared variables and message channels–Races must be explicitly avoided–Channels can be queued or rendezvous•Very C like7Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityExecutabilityNo difference between conditions and statements•Execution of every statement is conditional on its executability•Executability is the basic means of synchronizationDeclarations and assignments are always executableConditionals are executable when they holdThe following are the same•while (a != b) skip•(a == b)8Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityDelimitorsSemi-colon is used a statement separator not a statement terminator•Last statement does not need semi-colon•Often replaced by ! to indicate causality between two successive statements•(a == b); c = c + 1•(a == b) ! c = c + 19Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityData TypesBasic : bit/bool, byte, short, int, chanArrays: fixed size•byte state[20];•state[0] = state[3 * i] + 5 * state[7/j];Symbolic constants•Usually used for message types•mtype = {SEND, RECV};10Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityProcess Definitionbyte state = 2;proctype A() { (state == 1) ! state = 3 }proctype B() { state = state – 1 }11Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityProcess Instantiationbyte state = 2;proctype A() { (state == 1) ! state = 3 }proctype B() { state = state – 1 }init { run A(); run B() }run can be used anywhererun can be used anywhereSample 112Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityProcess Parameterizationbyte state = 1proctype A(byte x; short foo) { (state == 1 && x > 0) ! state = foo }init { run A(1,3); }Data arrays or processes cannot be passedData arrays or processes cannot be passedSample 213Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityRace Conditionbyte state = 1;proctype A() { byte x = state; x = x + 1; state = x;}proctype B() { byte y = state; y = y + 2; state = y;}init { run A(); run B() }Sample 314Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityDeadlockbyte state = 2;proctype A() { (state == 1) ! state = state + 1}proctype B() { (state == 1) ! state = state – 1}init { run A(); run B() }Sample 415Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityAtomic sequencesbyte state = 1;proctype A() { atomic { byte x = state; x = x + 1; state = x; }}byte state = 1;proctype A() { atomic { byte x = state; x = x + 1; state = x; }}proctype B() { atomic { byte y = state; y = y + 2; state = y; }}init { run A(); run B() }proctype B() { atomic { byte y = state; y = y + 2; state = y; }}init { run A(); run B() }Sample 516Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityMessage passingChannel declaration•chan qname = [16] of {short}•chan qname = [5] of {byte,int,chan,short}Sending messages•qname!expr•qname!expr1,expr2,expr3Receiving messages•qname?var•qname?var1,var2,var317Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityMessage passingMore parameters sent•Extra parameters droppedMore parameters received•Extra parameters undefinedFewer parameters sent•Extra parameters undefinedFewer parameters received•Extra parameters dropped18Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityMessage passingchan x = [1] of {byte,byte};chan y = [1] of {byte,byte};proctype A(byte p, byte q) { x!p,q ; y?p,q }chan x = [1] of {byte,byte};chan y = [1] of {byte,byte};proctype A(byte p, byte q) { x!p,q ; y?p,q }proctype B() { byte p,q; x?p,q ; y!q,p }init { run A(5,7); run B() }proctype B() { byte p,q;


View Full Document
Download Lecture
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 Lecture 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 Lecture 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?