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

This is the first introductory textbook on Spin, the only requirement is a background in programming. Spin models are written in the Promela language which is easily learned by students and programmers. Spin is easy to install and use. The Spin model checker is not only a widely used professional tool but it is also a superb tool for teaching important concepts of computer science such as verification, concurrency and nondeterminism. The book introduces Spin-based software that the author has developed for teaching. Complete programs demonstrate each construct and concept and these programs are available on a companion website.