Specifying Systems

The TLA+ language and tools for hardware and software engineers

Leslie Lamport

380 pages, parution le 07/10/2002

Ajouter à une liste

Indisponible

Résumé

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.

Contents
Part I Getting Started

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

Part II More Advanced Topics

9 Real Time
10 Composing Specifications
11 Advanced Examples

Part III The Tools

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

Part IV The TLA[superscript +] Language

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

Caractéristiques techniques

	PAPIER
Éditeur(s)	Addison Wesley
Auteur(s)	Leslie Lamport
Parution	07/10/2002
Nb. de pages	380
Format	18,7 x 23,2
Couverture	Broché
Poids	580g
Intérieur	Noir et Blanc
EAN13	9780321143068