Leslie Lamport's "Specifying Systems" argues that engineers can use the TLA+ language to precisely define the safety properties of hardware and software systems. The book serves as both a tutorial and a comprehensive reference for TLA+, detailing the language and its associated tools. It emphasizes writing specifications for systems, with the first part covering essential knowledge for most programmers and engineers. The second part introduces advanced topics such as liveness and fairness properties, real-time considerations, and system composition.
The reader will learn to write system specifications and gain a detailed understanding of TLA+. The book is structured to provide foundational knowledge for general engineering use, alongside advanced material for more complex system analysis. It offers a complete reference to the TLA+ language and its tools, making it a valuable resource for those involved in system design and verification.
Key concepts
- TLA+ — A language for writing specifications of systems.
- Safety properties — A class of system properties that the book emphasizes.
- Liveness properties — Advanced topics covered in the second part of the book.
- Fairness properties — Advanced topics covered in the second part of the book.
- Real-time properties — Advanced topics covered in the second part of the book.
- Composition — Advanced topics covered in the second part of the book.