Principles of the Spin Model Checker (Paperback)

Foreword.- Preface.- Sequential Programming in PROMELA.- A First Program in PROMELA.- Random Simulation- Data Types.- Operators and Expressions.- Control Statements.- Repetitive Statements.- Jump Statements.- Verification of Sequential Programs.- Assertions.- Verifying a program in Spin.- Concurrency.- Interleaving.- Atomicity.- Interactive Simulation.- Interference between processes.- Sets of Processes.- Interference revisited.- Deterministic Sequences of Statements.- Verification with Assertions.- The critical section problem.- Synchroniztion.- Synchronization by blocking.- Executability of statements.- State transition diagrams.- Atomic sequences of statements.- Semaphores.- Nondeterminism in models of concurrent systems.- Termination of Processes.- Verification with Temporal Logic.- Beyond Assertions.- Introduction to linear temporal logic.- Safety properties.- Liveness properties.- Fairness.- Duality.- Verifying correctness without ghost variables.- Modeling a non-critical section.- Advanced temporal specifications.- Data and Program Structures.- Arrays.- Type Definitions.- The preprocessor.- Inline.- Channels.- Channels in PROMELA.- Rendezvous channels.- Buffered channels.- Checking the content of a channel.- Random receive .- Sorted send .- Copying the value of a message .- Polling .- Comparing rendezvous and buffered channels.- Nondeterminism .- Nondeterministic finite automata.- VN: Visualizing Nondeterminism.- NP problems.- Advanced Topics in PROMELA .- Specifiers for Variables.- Predefined variables.- Priority.- Modeling Exceptions.- Reading from standard input.- Embedded C code.- Advanced Topics in SPIN .- How SPIN searches the state space.- Optimizing the performances of verifications.- Never claims.- Non-progress cycles.- Case Studies .- Channels as data structures.- Nondeterministic algorithms.- Modeling a real-time scheduling algorithm.- Fischer's algorithm.- Modeling distributed systems.- The Chandy-Lamport algorithm for global snapshots.- TheChandy-Lamport snapshot algorithm in PROMELA.- Verification of the snapshot algorithm.- Appendix A: Software Tools.- Appendix B: Links.- References.- Index