Tools for TLA+ specifications.
The goal of this project is to develop methods and tools that will permit engineers to apply formal specification and verification to high-level designs of concurrent algorithms and systems. We believe this can significantly improve the design process:
- Specification forces a careful and rigorous examination of what an algorithm or system should do, separate from how it should do it.
- Verification can catch bugs in an algorithm or a system design even before it is implemented, where one wants to catch and correct it.
As systems get more complex and their high-level designs become a more significant source of errors, this work will become increasingly important.
TLA+ and Tools
In a previous incarnation, we developed
- The Temporal Logic of Action (TLA), a formalism that brings the full power of mathematics to specifying and reasoning about concurrent systems.
- TLA+, a complete formal language for TLA. TLA+ is a very expressive language for writing high-level specifications.
- A set of tools for TLA+, consisting of a TLA+ parser, a TLA+ pretty printer, and a model checker (TLC). The TLC model checker accepts a large subclass of TLA+ specifications--a class that appears to include the specifications that people write of real systems. It uses parallel execution to achieve almost linear speedup with multiple processors and/or multiple independent machines.
As part of this project, we have developed the TLA+ Toolbox: an IDE (Integrated Development Environment) for writing and editing TLA+ specifications and running the TLA+ tools on them. Most users will run the tools from the Toolbox, which is freely available; see the Toolbox Web Page for downloading and installation instructions. The TLA+ tools can also be run outside the Toolbox; see the TLA+ Tools web page for instructions to download, install, and run them.
There have been a number of applications of TLA/TLC. It has been used to study cache coherence protocols, memory models, network protocols, database protocols, and several concurrent algorithms. See the TLA web page for more information. The paper High-Level Specifications: Lessons from Industry describes the use of TLA and TLC by an Intel processor design group.
We are currently investigating possible uses of TLA at Microsoft. This is a mutual learning process--system designers have to understand TLA, and we have to understand the design process to help figure out how TLA can be used. We are currently working with the XML Web Services team on specifying and checking their protocols. We have written a TLA specification of the Web Services Atomic Transaction protocol, which has helped clarify some aspects of the protocol. This work is still in the preliminary stage.
TLAPS: A TLA+ Proof System
In a project that is part of the Microsoft-Inria Joint Centre, we are building TLAPS, a proof system for TLA+. We have extended the language to permit writing hierarchically structured proofs and have implemented a proof manager that can call various proof engines to check those proofs. TLAPS is run from the TLA+ Toolbox, but it must be downloaded separately. See the project's web page for more details. Non-Microsoft members of the project include Damien Doligez and Stephan Merz.
To address some of the limitations of TLC, we started working on BTLC, a SAT-based symbolic model checker for TLA+. Because BTLC represents the state space symbolically as a boolean formula, it should allow us to model check systems that TLC is not able to handle and, perhaps more important, to check inductive invariants.
A BTLC prototype was built in the summer of 2003. Preliminary experiments were encouraging. However, work on BTLC is on hold because the people working on it have moved on to other projects.
Yuan Yu (maintaining TLC)
Tom Rodeheffer (consulting for product groups)