| |
| |
Foreword | |
| |
| |
Preface | |
| |
| |
| |
Sequential Programming in Promela | |
| |
| |
| |
A first program in Promela | |
| |
| |
| |
Random simulation | |
| |
| |
| |
Data types | |
| |
| |
| |
Type conversions | |
| |
| |
| |
Operators and expressions | |
| |
| |
| |
Local variables | |
| |
| |
| |
Symbolic names | |
| |
| |
| |
Control statements | |
| |
| |
| |
Selection statements | |
| |
| |
| |
Conditional expressions | |
| |
| |
| |
Repetitive statements | |
| |
| |
| |
Counting loops | |
| |
| |
| |
Jump statements | |
| |
| |
| |
Verification of Sequential Programs | |
| |
| |
| |
Assertions | |
| |
| |
| |
Verifying a program in Spin | |
| |
| |
| |
Guided simulation | |
| |
| |
| |
Displaying a computation | |
| |
| |
| |
Concurrency | |
| |
| |
| |
Interleaving | |
| |
| |
| |
Displaying a computation | |
| |
| |
| |
Atomicity | |
| |
| |
| |
Interactive simulation | |
| |
| |
| |
Interference between processes | |
| |
| |
| |
Sets of processes | |
| |
| |
| |
Interference revisited | |
| |
| |
| |
Deterministic sequences of statements | |
| |
| |
| |
Verification with assertions | |
| |
| |
| |
The critical section problem | |
| |
| |
| |
Synchronization | |
| |
| |
| |
Synchronization by blocking | |
| |
| |
| |
Executability of statements | |
| |
| |
| |
State transition diagrams | |
| |
| |
| |
Atomic sequences of statements | |
| |
| |
| |
d_step and atomic | |
| |
| |
| |
Semaphores | |
| |
| |
| |
Nondeterminism in models of concurrent systems | |
| |
| |
| |
Generating values nondeterministically | |
| |
| |
| |
Generating from an arbitrary range | |
| |
| |
| |
Termination of processes | |
| |
| |
| |
Deadlock | |
| |
| |
| |
End states | |
| |
| |
| |
The order of process termination | |
| |
| |
| |
Verification with Temporal Logic | |
| |
| |
| |
Beyond assertions | |
| |
| |
| |
Introduction to linear temporal logic | |
| |
| |
| |
The syntax of LTL | |
| |
| |
| |
The semantics of LTL | |
| |
| |
| |
Safety properties | |
| |
| |
| |
Expressing safety properties in LTL | |
| |
| |
| |
Expressing safety properties in Promela | |
| |
| |
| |
Verifying safety properties in Spin | |
| |
| |
| |
Liveness properties | |
| |
| |
| |
Expressing liveness properties in Spin | |
| |
| |
| |
Verifying liveness properties in Spin | |
| |
| |
| |
Fairness | |
| |
| |
| |
Duality | |
| |
| |
| |
Verifying correctness without ghost variables | |
| |
| |
| |
Modeling a noncritical section | |
| |
| |
| |
Advanced temporal specifications | |
| |
| |
| |
Latching | |
| |
| |
| |
Infinitely often | |
| |
| |
| |
Precedence | |
| |
| |
| |
Overtaking | |
| |
| |
| |
Next | |
| |
| |
| |
Data and Program Structures | |
| |
| |
| |
Arrays | |
| |
| |
| |
Type definitions | |
| |
| |
| |
The preprocessor | |
| |
| |
| |
Condition compilation | |
| |
| |
| |
Macros | |
| |
| |
| |
Inline | |
| |
| |
| |
Channels | |
| |
| |
| |
Channels in Promela | |
| |
| |
| |
Channels and channel variables | |
| |
| |
| |
Rendezvous channels | |
| |
| |
| |
Reply channels | |
| |
| |
| |
Arrays of channels | |
| |
| |
| |
Local channels | |
| |
| |
| |
Limitations of rendezvous channels | |
| |
| |
| |
Buffered channels | |
| |
| |
| |
Checking the content of a channel | |
| |
| |
| |
Checking if a channel is full or empty | |
| |
| |
| |
Checking the number of messages in a channel | |
| |
| |
| |
Random receive | |
| |
| |
| |
Sorted send | |
| |
| |
| |
Copying the value of a message | |
| |
| |
| |
Polling | |
| |
| |
| |
Comparing rendezvous and buffered channels | |
| |
| |
| |
Nondeterminism | |
| |
| |
| |
Nondeterministic finite automata | |
| |
| |
| |
timeout | |
| |
| |
| |
Using verification to find accepting computations | |
| |
| |
| |
Finding all counterexamples | |
| |
| |
| |
[lambda]-transitions | |
| |
| |
| |
VN: Visualizing nondeterminism | |
| |
| |
| |
NP problems | |
| |
| |
| |
Advanced Topics in Promela | |
| |
| |
| |
Specifiers for variables | |
| |
| |
| |
Predefined variables | |
| |
| |
| |
The anonymous variable | |
| |
| |
| |
Process identifiers | |
| |
| |
| |
Priority | |
| |
| |
| |
Simulation priority | |
| |
| |
| |
Modeling priority with global constraints | |
| |
| |
| |
Modeling exceptions | |
| |
| |
| |
Reading from standard input | |
| |
| |
| |
Embedded C code | |
| |
| |
| |
Advanced Topics in Spin | |
| |
| |
| |
How Spin searches the state space | |
| |
| |
| |
Optimizing the performance of verifications | |
| |
| |
| |
Writing efficient models | |
| |
| |
| |
Allocating memory for the hash table | |
| |
| |
| |
Compressing the state vector | |
| |
| |
| |
Minimal automaton | |
| |
| |
| |
Partial-order reduction | |
| |
| |
| |
Never claims | |
| |
| |
| |
A never claim for a safety property | |
| |
| |
| |
A never claim for a liveness property | |
| |
| |
| |
Never claims for other LTL formulas | |
| |
| |
| |
Predefined constructs for use in never claims | |
| |
| |
| |
Non-progress cycles | |
| |
| |
| |
Case Studies | |
| |
| |
| |
Channels as data structures | |
| |
| |
| |
Nondeterministic algorithms | |
| |
| |
| |
The eight-queens problem | |
| |
| |
| |
Cycles in a directed graph | |
| |
| |
| |
Modeling a real-time scheduling algorithm | |
| |
| |
| |
Real-time systems | |
| |
| |
| |
Modeling a scheduler in Promela | |
| |
| |
| |
Simplifying the model | |
| |
| |
| |
Modeling a scheduler with priorities | |
| |
| |
| |
Rate monotonic scheduling | |
| |
| |
| |
Fischer's algorithm | |
| |
| |
| |
Modeling distributed systems | |
| |
| |
| |
The Chandy-Lamport algorithm for global snapshots | |
| |
| |
| |
The Chandy-Lamport snapshot algorithm in Promela | |
| |
| |
| |
Structure of the program | |
| |
| |
| |
Encoding lists of channels | |
| |
| |
| |
The environment node | |
| |
| |
| |
Local data for each node | |
| |
| |
| |
Nodes of the distributed system | |
| |
| |
| |
Nondeterministic choice of a channel | |
| |
| |
| |
Verification of the snapshot algorithm | |
| |
| |
| |
Software Tools | |
| |
| |
| |
Spin | |
| |
| |
| |
jSpin | |
| |
| |
| |
SpinSpider | |
| |
| |
| |
VN: Visualizing nondeterminism | |
| |
| |
| |
Links | |
| |
| |
References | |
| |
| |
Index | |