Mechanical Verification of Concurrent Systems with TLA
Urban Engberg
Peter Grønning
Aarhus University
Technical University of Denmark
Leslie Lamport
Digital Equipment Corporation
Systems Research Center
14 September 1992 – version 2
THIS PAGE SHOULD NOT APPEAR
IN THE CAV PROCEEDINGS.
All but this page to appear in Proceedings of the Fourth International Workshop on Computer-Aided Verification
Mechanical Verification of Concurrent Systems with TLA
Urban Engberg1 , Peter Grønning2 , and Leslie Lamport3
1
Aarhus University
Technical University of Denmark
3
Digital Equipment Corporation
Systems Research Center
2
Abstract. We describe an initial version of a system for mechanically checking the correctness proof of a concurrent system. Input to the system consists of the correctness properties, expressed in TLA (the temporal logic of actions), and their proofs, written in a humanly readable, hierarchically structured form. The system uses a mechanical verifier to check each step of the proof, translating the step’s assertion into a theorem in the verifier’s logic and its proof into instructions for the verifier.
Checking is now done by LP (the Larch Prover), using two different translations—one for action reasoning and one for temporal reasoning.
The use of additional mechanical verifiers is planned. Our immediate goal is a practical system for mechanically checking proofs of behavioral properties of a concurrent system; we assume ordinary properties of the data structures used by the system.
1
Introduction
TLA, the Temporal Logic of Actions, is a logic for specifying and reasoning about concurrent systems. Systems and their properties are described by logical formulas; the TLA formula Π ⇒ Φ asserts that the system represented by Π satisfies the property, or implements the system, represented by Φ. TLA is a linear-time temporal logic [4] that can express liveness (eventuality) as well as safety (invariance) properties. Although TLA is a formal logic, the TLA specification of a concurrent system is no more difficult to write than the system’s description in a conventional programming language.
Since TLA is a formal logic, it allows completely rigorous reasoning. It is clear that TLA proofs can, in principle, be checked mechanically. In 1991, we began a one-year effort to determine if mechanical verification with TLA is practical. We decided to use the LP verification system [1, 2], initially planning to write proofs directly in LP. However, we found the LP encoding to be distracting, making large proofs difficult. We therefore decided to write a TLA to LP translator, so specifications, theorems, and proof steps could be written in TLA.
Writing specifications and theorems directly in TLA avoids the errors that can be introduced when hand translating what one wants to prove into the language of a verifier. The translator also allows mechanically checked proofs to have the same structure as hand proofs, making them easier to write and understand.
2
Working on the translator has thus far allowed us time to verify only a few simple examples, including an algorithm to compute a spanning tree on an arbitrary graph. Experience with more realistic examples is needed to determine if mechanical verification of TLA formulas can be a practical tool for concurrentsystem design. It will never be easy to write rigorous proofs. However, we find it very encouraging that mechanically checkable proofs written in the translator seem to be only two to three times longer than careful hand proofs.
TLA, its LP encoding, and the translator are described in the following three sections, using the spanning-tree algorithm as an example. In this example, we prove that a system satisfies a property. An important feature of TLA is the ability to prove that one system implements (is a refinement of) another.
However, space does not permit an example of such a proof.
2
TLA
For the purposes of this paper, we can consider TLA to be ordinary predicate logic, except
