Leslie Lamport's book: "Specifying Systems"

Leslie Lamport - one of the Monster in theory of concurrent and distributed systems wrote a book "Specifying Systems" [PDF].

CONTENTS
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
8. Liveness and Fairness
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+
16. The Operators of TLA+
17. The Meaning of a Module
18. The Standard Modules

P.S. Book page contains a link on "The Wildfire Verification Challenge Problem".
P.P.S TLA - The Temporal Logic of Actions