Book description
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.
Table of contents
- Copyright
- Preface
- 1. Finding Bugs in Concurrent Systems
- 2. Building Verification Models
-
3. An Overview of PROMELA
- Types of Objects
- Processes
- Provided Clauses
- Data Objects
- Data Structures
- Message Channels
- Channel Poll Operations
- Sorted Send And Random Receive
- Rendezvous Communication
- Rules For Executability
- Assignments And Expressions
- Control Flow: Compound Statements
- Atomic Sequences
- Deterministic Steps
- Selection
- Repetition
- Escape Sequences
- Inline Definitions
- Reading Input
- Special Features
- Finding Out More
- 4. Defining Correctness Claims
-
5. Using Design Abstraction
- What Makes a Good Design Abstraction?
- Data and Control
- The Smallest Sufficient Model
- Avoiding Redundancy
- Counters
- Sinks, Sources, and Filters
- Simple Refutation Models
- Pathfinder
- A Disk-Head Scheduler
- Controlling Complexity
- Example
- A Formal Basis for Reduction
- Example – A File Server
- In Summary
- Bibliographic Notes
-
6. Automata and Logic
- Automata
- Omega Acceptance
- The Stutter Extension Rule
- Finite States, Infinite Runs
- Other Types of Acceptance
- Logic
- Temporal Logic
- Recurrence and Stability
- Using Temporal Logic
- Valuation Sequences
- Stutter Invariance
- Fairness
- From Logic To Automata
- An Example
- Omega-Regular Properties
- Other Logics
- Bibliographic Notes
- 7. PROMELA Semantics
- 8. Search Algorithms
- 9. Search Optimization
-
10. Notes on Model Extraction
- The Role of Abstraction
- From ANSI-C to PROMELA
- Embedded Assertions
- A Framework for Abstraction
- Sound and Complete Abstraction
- Selective Data Hiding
- Example
- Bolder Abstractions
- Dealing With False Negatives
- Thorny Issues With Embedded C Code
- The Model Extraction Process
- The Halting Problem Revisited
- Bibliographic Notes
-
11. Using SPIN
- SPIN Structure
- Roadmap
- Simulation
- Random Simulation
- Interactive Simulation
- Guided Simulation
- Verification
- Generating a Verifier
- Compiling the Verifier
- Tuning a Verification Run
- The Number of Reachable States
- Search Depth
- Cycle Detection
- Inspecting Error Traces
- Internal State Numbers
- Special Cases
- Disabling Partial Order Reduction
- Boosting Performance
- Separate Compilation
- Lowering Verification Complexity
- 12. Notes on XSPIN
- 13. The Timeline Editor
- 14. A Verification Model of a Telephone Switch
- 15. Sample SPIN Models
-
16. PROMELA Language Reference
- Name
- Syntax
- EXECUTABILITY
- EFFECT
- DESCRIPTION
- Examples
- Notes
- See Also
- Grammar Rules
- Main Sections
- Reference
- Special Cases
- _
- _last
- _nr_pr
- _pid
- accept
- active
- arrays
- assert
- assignment
- atomic
- break
- chan
- comments
- cond_expr
- condition
- d_step
- datatypes
- do
- else
- empty
- enabled
- end
- eval
- false
- float
- full
- goto
- hidden
- hierarchy
- if
- init
- inline
- labels
- len
- local
- ltl
- macros
- mtype
- nempty
- never
- nfull
- np_
- pc_value
- pointers
- poll
- printf
- priority
- probabilities
- procedures
- proctype
- progress
- provided
- rand
- real-time
- receive
- remoterefs
- run
- scanf
- send
- separators
- sequence
- show
- skip
- STDIN
- timeout
- trace
- true
- typedef
- unless
- xr
- 17. Embedded C Code
- 18. Overview of SPIN Options
- 19. Overview of PAN Options
- Literature
- A. Automata Products
-
B. The Great Debates
- Branching Time vs Linear Time
- Symbolic Verification vs Explicit Verification
- Breadth-First Search vs Depth-First Search
- Tarjan Search vs Nested Search
- Events vs States
- Realtime Verification vs Timeless Verification
- Probability vs Possibilty
- Asynchronous Systems vs Synchronous Systems
- Interleaving vs True Concurrency
- Open vs Closed Systems
- C. Exercises With SPIN
- D. Downloading Spin
- Tables and Figures
Product information
- Title: Spin Model Checker, The: Primer and Reference Manual
- Author(s):
- Release date: September 2003
- Publisher(s): Addison-Wesley Professional
- ISBN: 9780321228628
You might also like
book
Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS
A Step-by-Step Guide to Verification of Digital Systems This practical book provides a step-by-step, interactive introduction …
book
Cooperative Control of Multi-Agent Systems
Distributed controller design is generally a challenging task, especially for multi-agent systems with complex dynamics, due …
book
Expert F# 4.0, Fourth Edition
Learn from F#'s inventor to become an expert in the latest version of this powerful programming …
book
Advances in Computers
Advances in Computers, Volume 108, the latest volume in a series published since 1960, presents detailed …