Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers

by Leslie Lamport

This work 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 behavioural properties of a system - what that system is allowed to do. The emphasis here is on safety properties. The second part covers more advanced topics, including liveness and fairness, real time properties, and composition. The books final two parts provide a complete reference manual for the TLA+ language and tools, as well as a mini-manual.

Genres: Computer Science, Programming, Technical, Software, Technology, Mathematics, Computers

384 pages, Paperback

First published July 29, 2002

Reviews

[Max Lybbert]

I've been reading several books by mathematician programmers (Donal Knuth, Alexander Stepanov, Edsger Dijkstra), and one book about UML. TLA+ does what UML is supposed to: provide a solid foundation for designing and reasoning about programs. TLA+ is also designed to be typeset a la TeX and fed into validation programs. Unfortunately, I'm not a big fan of the ASCII representation.

Book's website (including errate, tools, and PDF version of book) is at http://www.tlaplus.net/documentation/... .

[Dave Peticolas]

A gentle introduction to specifying concurrent systems with the Temporal Logic of Actions, and the use of the TLC model checker to test them out.

[Bugzmanov]

Disclaimer: I've chickened out after getting to Advanced section. Lamport is at galaxy brain level with math.

But first section is great. It provided an awesome example how you can start with a basic toy spec and refine it until you get something useful and real.
This was very enlightening.

[Pawan]

First few chapters are interesting mathematics (called temporal logic) and later goes on to explain concurrency and sequential consistency. Later half of the book requires the supplementary material from author's website.