The Spin Model Checker: Primer and Reference Manual

The Spin Model Checker: Primer and Reference Manual

by Gerard J. Holzmann
     
 

View All Available Formats & Editions

ISBN-10: 0321228626

ISBN-13: 9780321228628

Pub. Date: 11/01/2003

Publisher: Addison-Wesley

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

Overview

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.

Product Details

ISBN-13:
9780321228628
Publisher:
Addison-Wesley
Publication date:
11/01/2003
Edition description:
New Edition
Pages:
608
Product dimensions:
7.10(w) x 9.60(h) x 1.32(d)

Table of Contents

Prefaceix
Introduction
1Finding Bugs in Concurrent Systems1
Circular Blocking
Deadly Embrace
Mismatched Assumptions
Fundamental Problems of Concurrency
Observability and Controllability
2Building Verification Models7
Introducing Promela
Some Examples
Biographical Notes
3An Overview of Promela33
Processes
Data Objects
Message Channels
Channel Poll Operations
Sorted Send and Random Receive
Rendezvous Communication
Rules for Executability
Control Flow
Finding out More
4Defining Correctness Claims73
Basic Types of Claims
Assertions
Meta-Labels
Fair Cycles
Never Claims
The Link with LTL
Trace Assertions
Predefined Variables and Functions
Path Quantification
Finding out More
5Using Design Abstraction101
What Makes a Good Design Abstraction?
Data and Control
The Smallest Sufficient Model
Avoiding Redundancy
Counters
Sinks
Sources
Filters
Simple Refutation Models
Examples
Controlling Complexity
A Formal Basis for Reduction
Foundation
6Automata and Logic127
Omega Acceptance
The Stutter Extension Rule
Finite States
Infinite Runs
Other Types of Acceptance
Temporal Logic
Recurrence and Stability
Valuation Sequences
Stutter Invariance
Fairness
From Logic to Automata
Omega-Regular Properties
Other Logics
Bibliographic Notes
7Promela Semantics153
Transition Relation
Operational Model
Semantics Engine
Interpreting Promela Models
Three Examples
Verification
The Never Claim
8Search Algorithms167
Depth-First Search
Checking Safety Properties
Depth-Limited Search
Trade-Offs
Breath-First Search
Checking Liveness Properties
Adding Fairness
The Spin Implementation
Complexity Revisited
Bibliographic Notes
9Search Optimization191
Partial Order Reduction
Visibility
Statement Merging
State Compression
Collapse Compression
The Minimized Automaton Representation
Bitstate Hashing
Bloom Filters
Hash-Compact
Bibliographic Notes
10Notes on Model Extraction217
The Role of Abstraction
From ANSI-C to Promela
Embedded Assertions
A Framework for Abstraction
Soundness and Completeness
Selective Data Hiding
Bolder Abstractions
Dealing with False Negatives
Thorny Issues with Embedded C Code
The Model Extraction Process
The Halting Problem Revisited
Bibliographic Notes
Practice
11Using Spin245
Spin Structure
Roadmap
Random Simulation
Interactive Simulation
Generating and Compiling a 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
12Notes on Xspin267
Starting a Session with Xspin
Menus
Syntax Checking
Property-Based Slicing
Simulation Parameters
Verification Parameters
The LTL Property Manager
The Automaton View Option
13The TimeLine Editor283
An Example
Types of Events
Defining Events
Matching a Timeline
Automata Definitions
Variations on a Theme
Constraints
Timelines with One Event
Timelines with Multiple Events
The Link with LTL
Bibliographic Notes
14A Verification Model of a Telephone Switch299
General Approach
Keeping it Simple
Managing Complexity
Subscriber Model
Switch Model
Remote Switches
Adding Features
Three-Way Calling
15Sample Spin Models325
The Sieve of Eratosthenes
Process Scheduling
A Client-Server Model
A Square-Root Server
Adding Interaction
Adding Assertions
A Comment Filter
Reference Material
16Promela Language Reference363
Grammar Rules
Special Cases
Promela Manual Pages
Meta Terms
Declarators
Control Flow Constructors
Basic Statements
Predefined Functions and Operators
Omissions
17Embedded C Code495
Example
Data References
Execution
Issues to Consider
Deferring File Inclusion
Manual Pages for Embedded C Code
18Overview of Spin Options513
Compile-Time Options
Simulation
Syntax-Checking
Postscript Generation
Model Checker Generation
LTL Conversion
Miscellaneous Options
19Overview of Pan Options527
Pan Compile-Time Options
Tuning Partial Order Reduction
Increasing Speed
Decreasing Memory Use
Debugging Pan Verifiers
Experimental Options
Pan Run-Time Options
Pan Output Format
Literature545
Appendices
AAutomata Products553
Asynchronous and Synchronous Products
Defining Atomic Sequences and Rendezvous
Expanded Asynchronous Products
Buchi Acceptance
Non-Progress
Deadlock
BThe Great Debates563
Branching vs Linear Time
Symbolic vs Explicit
Breadth-First vs Depth-First
Tarjan vs Nested
Events vs States
Realtime vs Timeless
Probability vs Possibility
Asynchronous vs Synchronous
Interleaving vs True Concurrency
Open vs Closed Systems
CExercises with Spin573
DDownloading Spin579
Tables and Figures581
Index585

Customer Reviews

Average Review:

Write a Review

and post it to your social network

     

Most Helpful Customer Reviews

See all customer reviews >