DOC PREVIEW
CMU CS 15414 - Automated Program Verification and Testing

This preview shows page 1-2-17-18-19-36-37 out of 37 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

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

CMU CS 15414 - Automated Program Verification and Testing

Download Automated Program Verification and Testing
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 Automated Program Verification and Testing 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 Automated Program Verification and Testing 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?