This long-awaited book shows how to write unambiguous specifications of complex computer systems. The first part provides a concise and lucid introduction to specification, explaining how to describe, with mathematical precision, the behavioral properties of a system -- what that system is allowed to do. The emphasis here is on safety properties. The second part of the book covers more advanced topics, including liveness and fairness, real-time properties, and composition. The book's final two parts provide a complete reference manual for the TLA+ language and tools, as well as a handy minimanual. TLA+ is the language developed by the author for writing simple and elegant specifications of algorithms and protocols and for verifying the correctness of a design. The language already has proved to be a valuable aid in understanding and building concurrent and distributed systems. Tools for TLA+ syntax analysis and model checking are freely available from the Web, where you can also find supplemental materials for this book, including exercises.

• 1 A Little Simple Math
• 2 Specifying a Simple Clock
• 3 An Asynchronous Interface
• 4 A Fifo
• 5 A Caching Memory
• 6 Some More Math
• 7 Writing a Specification: Some Advice

• 9 Real Time
• 10 Composing Specifications
• 11 Advanced Examples

• 12 The Syntactic Analyzer
• 13 The TLATEX Typesetter
• 14 The TLC Model Checker

• 15 The Syntax of TLA[superscript +]
• 16 The Operators of TLA[superscript +]
• 17 The Meaning of a Module
• 18 The Standard Modules