## Specifying Systems: The TLA+ Language and Tools for Hardware and Software EngineersThis 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. |

### What people are saying - Write a review

#### Review: Specifying Systems: The Tla+ Language and Tools for Hardware and Software Engineers

User Review - Dave Peticolas - GoodreadsA gentle introduction to specifying concurrent systems with the Temporal Logic of Actions, and the use of the TLC model checker to test them out. Read full review

#### Review: Specifying Systems: The Tla+ Language and Tools for Hardware and Software Engineers

User Review - Max Lybbert - GoodreadsI'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 ... Read full review

### Contents

A Little Simple Math | 9 |

Specifying a Simple Clock | 15 |

An Asynchronous Interface | 23 |

Copyright | |

14 other sections not shown

### Common terms and phrases

alternating bit protocol arity ASCII asserts assigns behavior satisfying BNF grammar Boolean C-basic chan Channel Chapter CHOOSE component condition configuration file conjunction constant contains ctl[p Data declared defined definition described directed graph domain element ENABLED equals equivalent error evaluate example existential quantification expression FALSE FIFO finite function G.Expression graph HCini hour clock identifier implies Init initial predicate instantiation invariant level-correct lexemes linearizable mathematics meaning memInt memory specification memQ module n-tuple natural numbers next-state action opld opOrder parameter predicate logic Proc processor propositional logic quantifier real numbers real-time represent request Rsp(p sBit Section semantics Send sender sequence Serializable Spec statement string submodule SUBSET symbol symmetry set syntactically tautology temporal formula temporal logic theorem TLATgX TLC value true iff tuple TypeInvariant unchanged variables weak fairness wmem write-through cache