SPIN: Part 1© 2011 Carnegie Mellon University15-414 Bug Catching: Automated Program Verification and TestingSagar ChakiOctober 31, 2011What is This All About?Spin• On-the-fly verifier developed at Bell-labs by Gerard Holzmann and others• http://spinroot.comPromela2Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityPromela• Modeling language for SPIN• Targeted at asynchronous systems– Switching protocols• http://spinroot.com/spin/Man/Quick.htmlHistoryWork leading to Spin started in 1980• First bug found on Nov 21, 1980 by Pan• One-pass verifier for safety propertiesSucceeded by•Pandora(82), 3Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University•Pandora(82), • Trace (83), • SuperTrace (84), • SdlValid (88), • Spin (89)Spin covered omega-regular propertiesSpin CapabilitiesInteractive simulation• For a particular path• For a random pathExhaustive verification•Generate C code for verifier4Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University•Generate C code for verifier• Compile the verifier and execute• Returns counter-exampleLots of options for fine-tuningSpin Overall StructureGUIFront-endGUIFront-endPromelaParserPromelaParserLTL Parser andTranslatorSyntaxSyntaxInteractiveInteractive5Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityReportsSyntaxErrorReportsSimulationInteractiveSimulationVerifierGeneratorVerifierGeneratorOptimized ModelChecker (ANSI C)Executable O-T-FVerifierCounter ExamplePromelaStands for Process Meta LanguageLanguage for asynchronous programs• Dynamic process creation• Processes execute asynchronously•Communicate via shared variablesand messagechannels6Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University•Communicate via shared variablesand messagechannels– Races must be explicitly avoided– Channels can be queued or rendezvous• Very C likeExecutabilityNo 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 executable7Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityConditionals are executable when they holdThe following are the same• while (a != b) skip• (a == b)DelimitorsSemi-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 8Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University•Often replaced by →to indicate causality between two successive statements• (a == b); c = c + 1• (a == b) → c = c + 1Data TypesBasic : bit/bool, byte, short, int, chanArrays: fixed size• byte state[20];• state[0] = state[3 * i] + 5 * state[7/j];9Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversitySymbolic constants• Usually used for message types• mtype = {SEND, RECV};Process Definitionbyte state = 2;proctype A() { (state == 1) → state = 3 }10Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityproctype B() { state = state – 1 }Process Instantiationbyte state = 2;proctype A() { (state == 1) → state = 3 }Sample 111Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityproctype B() { state = state – 1 }init { run A(); run B() }run can be used anywhereProcess Parameterizationbyte state = 1proctype A(byte x; short foo) { (state == 1 && x > 0) → state = fooSample 212Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University}init { run A(1,3); }Data arrays or processes cannot be passedRace Conditionbyte state = 1;proctype A() {byte x = state;x = x + 1;state = x;}Sample 313Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityproctype B() {byte y = state;y = y + 2;state = y;}init { run A(); run B() }Deadlockbyte state = 2;proctype A() {(state == 1) → state = state + 1}Sample 414Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityproctype B() {(state == 1) → state = state – 1}init { run A(); run B() }Atomic sequencesbyte state = 1;proctype A() {atomic {byte x = state;x = x + 1;proctype B() {atomic {byte y = state;y = y + 2;state = y;}Sample 515Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityx = x + 1;state = x;}}}}init { run A(); run B() }Message passingChannel declaration• chan qname = [16] of {short}• chan qname = [5] of {byte,int,chan,short}Sending messages•qname!expr16Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University•qname!expr• qname!expr1,expr2,expr3Receiving messages• qname?var• qname?var1,var2,var3Message passingMore parameters sent• Extra parameters droppedMore parameters received• Extra parameters undefined17Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityFewer parameters sent• Extra parameters undefinedFewer parameters received• Extra parameters droppedMessage passingchan x = [1] of {byte,byte};chan y = [1] of {byte,byte};proctype A(byte p, byte q) { x!p,q; proctype B() { byte p,q;x?p,q ; y!q,p}init { Sample 618Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityx!p,q; y?p,q}init { run A(5,7); run B() }Message passingConvention: first message field often specifies message type (constant)Alternatively send message type followed by list of message fields in braces•qname!expr1(expr2,expr3)19Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University•qname!expr1(expr2,expr3)• qname?var1(var2,var3)ExecutabilitySend is executable only when the channel is not fullReceive is executable only when the channel is not emptyOptionally some arguments of receive can be constants• qname?RECV,var,1020Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University• Value of constant fields must match value of corresponding fields of message at the head of channel queuelen(qname) returns the number of messages currently stored in qnameIf
View Full Document