The spin model checker : primer and reference manual

The Spin Model Checker Is Used For Both Teaching Software Verification Techniques, And For Validating Large Scale Applications. The Growing Number Of Users Has Created A Need For A More Comprehensive User Guide And A Standard Reference Manual That Describes The Most Recent Version Of The Tool. This Book Fills That Need. Spin Is Used In Over 40 Countries. The Offical Spin Web Site, Spinroot.com Receives Between 2500 And 3000 Hits Per Day. It Has Been Estimated That Up To Three-quarters Of The $400 Billion Spent Annually To Hire Programmers In The United States Is Ultimately Spent On Debugging. 1. Finding Bugs In Concurrent Systems -- 2. Building Verification Models -- 3. An Overview Of Promela -- 4. Defining Correctness Claims -- 5. Using Design Abstraction -- 6. Automata And Logic -- 7. Promela Semantics -- 8. Search Algorithms -- 9. Search Optimization -- 10. Notes On Model Extraction -- 11. Using Spin -- 12. Notes On Xspin -- 13. The Timeline Editor -- 14. A Verification Model Of A Telephone Switch -- 15. Sample Spin Models -- 16. Promela Language Reference -- 17. Embedded C Code -- 18. Overview Of Spin Options -- 19. Overview Of Pan Options -- App. A. Automata Products -- App. B. The Great Debates -- App. C. Exercises With Spin -- App. D. Downloading Spin. Gerald J. Holzmann. Includes Bibliographical References And Index. Main Page 1 Table of content 2 Copyright 10 Preface 13 Logic Model Checking 14 The SPIN Model Checker 15 Book Structure 16 Chapter 1. Finding Bugs in Concurrent Systems 17 'Circular Blocking' 18 'Deadly Embrace' 19 'Mismatched Assumptions' 20 'Fundamental Problems of Concurrency' 21 Chapter 2. Building Verification Models 22 'SPIN' 23 'PROMELA' 24 Examples 25 'Hello World' 26 'Producers and Consumers' 29 'Extending the Example' 32 'Mutual Exclusion' 35 'Message Passing' 38 In Summary 41 Bibliographic Notes 42 Chapter 3. An Overview of PROMELA 43 'Types of Objects' 46 Processes 47 'Provided Clauses' 50 Data Objects 51 'Data Structures' 54 Message Channels 57 'Channel Poll Operations' 60 'Sorted Send And Random Receive' 61 'Rendezvous Communication' 62 Rules For Executability 65 'Assignments And Expressions' 68 Control Flow: Compound Statements 71 'Atomic Sequences' 72 'Deterministic Steps' 75 'Selection' 76 'Repetition' 79 'Escape Sequences' 82 'Inline Definitions' 85 'Reading Input' 88 'Special Features' 91 Finding Out More 94 Chapter 4. Defining Correctness Claims 95 'Stronger Proof' 96 Basic Types of Claims 97 'Basic Assertions' 98 'Meta Labels' 101 'Fair Cycles' 104 Never Claims 107 'The Link With LTL' 110 Trace Assertions 111 'Notrace' 114 Predefined Variables and Functions 115 'Remote Referencing' 118 Path Quantification 119 'Formalities' 120 Finding Out More 123 Chapter 5. Using Design Abstraction 124 'What Makes a Good Design Abstraction?' 125 'Data and Control' 126 'The Smallest Sufficient Model' 129 'Avoiding Redundancy' 130 'Counters' 131 'Sinks, Sources, and Filters' 132 'Simple Refutation Models' 135 'Pathfinder' 136 'A Disk-Head Scheduler' 139 Controlling Complexity 142 'Example' 143 'A Formal Basis for Reduction' 146 'Example – A File Server' 147 In Summary 150 Bibliographic Notes 151 Chapter 6. Automata and Logic 152 Automata 153 'Omega Acceptance' 156 'The Stutter Extension Rule' 157 'Finite States, Infinite Runs' 158 'Other Types of Acceptance' 159 Logic 160 'Temporal Logic' 163 'Recurrence and Stability' 166 'Using Temporal Logic' 169 'Valuation Sequences' 170 'Stutter Invariance' 171 'Fairness' 174 From Logic To Automata 175 'An Example' 178 'Omega-Regular Properties' 181 'Other Logics' 182 Bibliographic Notes 183 Chapter 7. PROMELA Semantics 184 Transition Relation 185 Operational Model 188 'Operational Model, Semantics Engine' 191 Interpreting PROMELA Models 194 'Three Examples' 195 Verification 198 'The Never Claim' 199 Chapter 8. Search Algorithms 200 'Depth-First Search' 201 Checking Safety Properties 204 'Depth-Limited Search' 207 'Trade-Offs' 210 'Breadth-First Search' 212 Checking Liveness Properties 215 'Adding Fairness' 218 The SPIN Implementation 221 Complexity Revisited 222 Bibliographic Notes 223 Chapter 9. Search Optimization 224 Partial Order Reduction 225 'Visibility' 228 Statement Merging 229 State Compression 232 'Collapse Compression' 233 'Minimized Automaton Representation' 236 'Bitstate Hashing' 239 'Bloom Filters' 242 'Hash-Compact' 245 Bibliographic Notes 248 Chapter 10. Notes on Model Extraction 249 The Role of Abstraction 250 From ANSI-C to PROMELA 251 'Embedded Assertions' 254 A Framework for Abstraction 255 'Sound and Complete Abstraction' 258 'Selective Data Hiding' 261 'Example' 262 'Bolder Abstractions' 265 Dealing With False Negatives 268 Thorny Issues With Embedded C Code 269 The Model Extraction Process 270 The Halting Problem Revisited 272 Bibliographic Notes 275 Chapter 11. Using SPIN 278 'SPIN Structure' 279 'Roadmap' 280 Simulation 283 'Random Simulation' 284 'Interactive Simulation' 287 'Guided Simulation' 290 Verification 291 'Generating a Verifier' 292 'Compiling the Verifier' 293 'Tuning a Verification Run' 296 'The Number of Reachable States' 297 'Search Depth' 300 'Cycle Detection' 303 'Inspecting Error Traces' 304 'Internal State Numbers' 307 Special Cases 308 'Disabling Partial Order Reduction' 309 'Boosting Performance' 310 'Separate Compilation' 313 'Lowering Verification Complexity' 316 Chapter 12. Notes on XSPIN 319 'Starting a Session With XSPIN' 320 The File Menu 323 The Edit Menu 324 The Help Menu 325 The Run Menu 326 'Syntax Check' 327 'Property-Based Slicing' 328 'Set Simulation Parameters' 329 '(Re)Run Simulation' 332 'Set Verification Parameters' 333 '(Re)Run Verification' 336 'LTL Property Manager' 337 'The Automaton View Option' 340 'In Summary' 343 Chapter 13. The Timeline Editor 344 An Example 345 Types of Events 346 Defining Events 347 Matching a Timeline 348 Automata Definitions 349 Constraints 350 Variations on a Theme 351 Timelines With One Event 354 Timelines With Multiple Events 355 The Link With LTL 358 Bibliographic Notes 361 Chapter 14. A Verification Model of a Telephone Switch 362 General Approach 363 'Keep it Simple' 364 'Managing Complexity' 365 Modeling a Switch 366 'Subscriber Model' 367 'Switch Model' 370 'Remote Switches' 373 Adding Features 376 'Three-Way Calling' 377 'A Three-Way Calling Scenario' 380 In Summary 383 Chapter 15. Sample SPIN Models 384 'Eratosthenes' 385 'Process Scheduling' 388 'A Client-Server Model' 391 'Square Roots?' 394 'Adding Interaction' 397 'Adding Assertions' 400 'A Comment Filter' 403 Chapter 16. PROMELA Language Reference 406 Chapter 16. PROMELA Language Reference 407 Syntax 408 EXECUTABILITY 409 EFFECT 410 DESCRIPTION 411 Examples 412 Notes 413 See Also 414 Grammar Rules 415 Main Sections 418 Reference 419 Special Cases 420 _ 423 _last 424 _nr_pr 427 _pid 428 accept 431 active 434 arrays 437 assert 440 assignment 443 atomic 446 break 449 chan 450 comments 453 cond_expr 456 condition 459 d_step 460 datatypes 463 do 466 else 469 empty 472 enabled 475 end 476 eval 479 false 482 float 483 full 486 goto 488 hidden 491 hierarchy 492 if 493 init 496 inline 499 labels 502 len 505 local 506 ltl 507 macros 510 mtype 513 nempty 516 never 517 nfull 520 np_ 521 pc_value 523 pointers 525 poll 526 printf 528 priority 531 probabilities 533 procedures 534 proctype 537 progress 538 provided 541 rand 543 real-time 546 receive 547 remoterefs 550 run 553 scanf 556 send 557 separators 560 sequence 561 show 563 skip 564 STDIN 567 timeout 569 trace 572 true 575 typedef 576 unless 579 xr 582 Chapter 17. Embedded C Code 585 An Example 586 Data References 588 Execution 591 Issues to Consider 594 Deferring File Inclusion 597 c_code 598 c_decl 601 c_expr 604 Chapter 18. Overview of SPIN Options 607 Compile-Time Options 608 Simulation Options 611 Syntax Checking Options 614 Postscript Generation 615 Model Checker Generation 616 LTL Conversion 619 Miscellaneous Options 620 Chapter 19. Overview of P'AN' Options 623 P'AN' Compile-Time Options 624 'Basic Options' 625 'Options Related to Partial Order Reduction' 628 'Options Used to Increase Speed' 629 'Options Used to Decrease Memory Use' 630 'Options to Use When Prompted by P'AN'' 631 'Options for Debugging P'AN' Verifiers' 632 'Experimental Options' 633 P'AN' Run-Time Options 636 P'AN' Output Format 639 Literature 642 Appendix A. Automata Products 645 'Asynchronous Products' 648 'Encoding Atomic Sequences' 649 'Rendezvous' 650 'Synchronous Products' 651 'An Example' 652 'Non-Progress Cycles' 655 'Deadlock Detection' 656 Appendix B. The Great Debates 657 'Branching Time vs Linear Time' 658 'Symbolic Verification vs Explicit Verification' 661 'Breadth-First Search vs Depth-First Search' 662 'Tarjan Search vs Nested Search' 663 'Events vs States' 664 'Realtime Verification vs Timeless Verification' 665 'Probability vs Possibilty' 666 'Asynchronous Systems vs Synchronous Systems' 667 'Interleaving vs True Concurrency' 668 'Open vs Closed Systems' 669 Appendix C. Exercises With SPIN 670 'C.1.' 671 'C.2.' 672 'C.3.' 673 'C.4.' 674 'C.5.' 675 'C.6.' 676 'C.7.' 677 'C.8.' 678 'C.9.' 679 Appendix D. Downloading Spin 682 LTL Conversion 683 Model Extraction 684 Timeline Editor 685 Tables and Figures 686 Tables 687 Figures 688 Master SPIN, the breakthrough tool for improving software reliability SPIN is the world's most popular, and arguably one of the world's most powerful, tools for detecting software defects in concurrent system designs. Literally thousands of people have used SPIN since it was first introduced almost fifteen years ago. The tool has been applied to everything from the verification of complex call processing software that is used in telephone exchanges, to the validation of intricate control software for interplanetary spacecraft. This is the most comprehensive reference guide to SPIN, written by the principal designer of the tool. It covers the tool's specification language and theoretical foundation, and gives detailed advice on methods for tackling the most complex software verification problems. Sum Design and verify both abstract and detailed verification models of complex systems software Sum Develop a solid understanding of the theory behind logic model checking Sum Become an expert user of the SPIN command line interface, the Xspin graphical user interface, and the TimeLine editing tool Sum Learn the basic theory of omega automata, linear temporal logic, depth-first and breadth-first search, search optimization, and model extraction from source code The SPIN software was awarded the prestigious Software System Award by the Association for Computing Machinery (ACM), which previously recognized systems such as UNIX, SmallTalk, TCP/IP, Tcl/Tk, and the World Wide Web