| |
| |
| 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 | |