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.

The TLA+ tools are freely available. Please go to the TLA+ Tools web page for instructions to download, install, and run the tools.

Applications

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.

A TLA+ Prover

In a project that is part of the Microsoft-Inria Joint Centre, we have begun building a proof system for TLA+. The project involves extending the language to permit writing hierarchically structured proofs and implementing a proof manager that can call various proof engines to check those proofs. Non-Microsoft members of the project are Kaustuv Chadhuri, Damien Doligez, and Stephan Merz. See the project's web page for more details.

BTLC

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.

Project Members

Leslie Lamport
Yuan Yu (maintaining TLC)
Tom Rodeheffer (consulting for product groups)