The Module Structure of TLA+
12 September 1996
An html document that informally describes the revised syntax and
semantics for the module structure of TLA+. This is a preliminary
draft; there have been a few minor changes to TLA+ since this was written.
(About 15 pages)
The
Operators of TLA+
12 April 1997
This document is an introduction to the syntax and semantics of
the operators of TLA+. It assumes that you are familiar with ordinary
mathematics (sets and functions) and are at least acquainted with TLA.
It should enable you to understand the expressions that appear in TLA+
specifications. Most of this information appears in
Specifying Concurrent Systems with TLA+,
with a couple of very minor changes. (20 pages)
Refinement in State-Based Formalisms
18 December 1996
A note explaining what refinement and dummy variables
are all about. It also sneaks in an introduction to
TLA. (7 pages)
Processes are in the Eye of the Beholder
Leslie Lamport
16 January 1996
An illustration of the power of TLA for transforming
algorithms.
A two-process algorithm is shown to be equivalent to an N-process
one, illustrating the insubstantiality of processes. A completely
formal equivalence proof in TLA (the Temporal Logic of Actions) is
sketched.
Appeared in Theoretical Computer Science, 179
(1997), 333-351.
Postscript -
DVI -
LaTeX
Proving Possibility Properties
Leslie Lamport
4 July 1995
Abstract: A method is described for proving
"always possibly" properties of specifications in formalisms with
linear-time trace semantics. It is shown to be relatively complete for
TLA (Temporal Logic of Actions) specifications.
To appear in Theoretical Computer Science
Postscript -
DVI -
LaTeX
Win32 Threads API
Specification
14 May 1996
A preliminary, unfinished TLA+ specification of the kernel
threads procedures from the Windows Win32 Application Programming
Interface (API). Win32 is the API for the Windows 95 and Windows NT
operating systems. This document shows what a real-world
specification looks like. It also illustrates how one can
write an "object oriented" specification in TLA+.
A TLA Solution to the RPC-Memory Specification Problem
Martín Abadi, Leslie Lamport, and Stephan Merz
16 January 1996
Presents a TLA solution to a specification and verification problem
proposed at a Dagstuhl workshop. (45 pages, with
index)
Appeared in Formal Systems Specification: The RPC-Memory
Specification Case Study. Manfred Broy,
Stephan Merz, and Katharina Spies editors.
LNCS 1169, (1996), 21-66.
LaTeX -
Postscript -
DVI
Click here for more information.
Lazy Caching in TLA
Peter Ladkin, Leslie Lamport, Bryan Olivier, and Denis Roegel
8 February 1999
We address the problem, proposed by Gerth, of verifying that the
simplified version of the lazy caching algorithm of Afek, Brown, and
Merritt, described
informally in
-
Verifying Sequential Consistent Memory Problem Definition
Rob Gerth
April 1993
Postscript
is sequentially consistent. We specify the algorithm and
sequential consistency in TLA+, a formal specification language based
on TLA (the Temporal Logic of Actions). We then describe a formal
correctness proof in TLA. (50 pages)
Appeared in Distributed Computing 12, 2/3, 1999, 151-174.
Postscript -
DVI
An Old-Fashioned Recipe for Real Time
Martin Abadi and Leslie Lamport
22 December 1993
Abstract:
Traditional methods for specifying and reasoning about concurrent
systems work for real-time systems. Using TLA (the temporal logic of
actions), we illustrate how they work with the examples of a queue and
of a mutual-exclusion protocol. In general, two problems must be
addressed: avoiding the real-time programming version of Zeno's
paradox, and coping with circularities when composing real-time
assumption/guarantee specifications. Their solutions rest on
properties of machine closure and realizability.
Appeared in ACM Toplas 16, 5 (September, 1994) 1543-1571
Postscript -
DVI -
LaTeX
Conjoining Specifications
Martin Abadi and Leslie Lamport
3 November 1995
This paper describes how to write and reason about open system
specifications--also known as
rely/guarantee specifications. It is rather hard going,
but Section 2 gives a simple introduction to the issues.
Abstract:
We show how to specify components of concurrent systems. The
specification of a system is the conjunction of its components'
specifications. Properties of the system are proved by reasoning
about its components. We consider both the decomposition of a given
system into parts, and the composition of given parts to form a
system.
Appeared in ACM Toplas 17, 3 (May, 1995) 507-534
Postscript -
DVI -
LaTeX
(requires acmtrans.sty)
TLA in Pictures
Leslie Lamport
31 August 1994
Other formalisms and informalisms no longer have all the
fun. Now, you can draw pictures of TLA specifications.
Abstract:
Predicate-action diagrams, which are similar to conventional
state-transition diagrams, are defined as representations of formulas
in the temporal logic of actions (TLA). These diagrams can be used to
express formal properties of specifications and to illustrate
correctness proofs. (8 large pages)
Appeared in IEEE Transactions on Software Engineering 21,
9, (September 1995) 768-775
Postscript -
DVI -
LaTeX (requires
IEEEtran.sty)
There is a minor error in this paper that no-one else seems
to have noticed.
Hybrid Systems in TLA+
Leslie Lamport
6 April 1993
Here is the famous gas burner of Ravn, Rischel, and Hansen
done in TLA+. This paper shows how to formally specification and
reason about solutions to integral (as in integral calculus)
equations.
Abstract:
\TLA+ is a general purpose, formal specification language based on the
Temporal Logic of Actions, with no built-in primitives for specifying
real-time properties. Here, we use \TLA+ to define operators for
specifying the temporal behavior of physical components obeying
integral equations of evolution. These operators, together with
previously defined operators for describing timing constraints, are
used to specify a toy gas burner introduced by Ravn, Rischel, and
Hansen. The burner is specified at three levels of abstraction, each
of the two lower-level specifications implementing the next
higher-level one. Correctness proofs are sketched.
Appeared in Hybrid Systems, edited by
Grossman, Nerode, Ravn, and Rischel, LNCS 736.
Postscript -
DVI -
LaTeX
Specifying and Verifying Fault-Tolerant Systems
Leslie Lamport and Stephan Merz
14 October 1994
Abstract: We formally specify a well known solution to the
Byzantine generals problem and give a rigorous, hierarchically
structured proof of its correctness. We demonstrate that this is
an engineering exercise, requiring no new scientific ideas.
Appeared in Formal Techniques in Real-Time and Fault-Tolerant
Systems. H. Langmaack, W.-P. de Roever, and J. Vytopil,
editors. LNCS 863, 41-76..
Postscript -
DVI -
LaTeX
Verification of a Multiplier: 64 Bits and Beyond
R. P. Kurshan and Leslie Lamport
14 April 1993
This is the first application of a general method, described in
"Conjoining Specifications", for
splitting off finite-state parts of a non-finite-state verification
problem for verification by a model checker.
Abstract:
Verifying a 64-bit multiplier has a computational complexity that puts
it beyond the grasp of current finite-state algorithms, including
those based upon homomorphic reduction, the induction principle, and
bdd fixed-point algorithms. Theorem proving, while not bound by the
same computational constraints, may not be feasible for routinely
coping with the complex, low-level details of a real multiplier. We
show how to verify such a multiplier by applying COSPAN, a
model-checking algorithm, to verify local properties of the complex
low-level circuit, and using TLP, a theorem prover based on the
Temporal Logic of Actions, to prove that these properties imply the
correctness of the multiplier. Both verification steps are automated,
and we plan to mechanize the translation between the languages of TLP
and COSPAN.
Appeared in Proceedings of the Fifth International Conference,
CAV'93. LNCS 697, 166-179.
Postscript -
DVI -
LaTeX
Mechanical Verification of Concurrent Systems with TLA
Urban Engberg, Peter Groenning, and Leslie Lamport
14 September 1992
This describes a now obsolete version of TLP, the mechanical
verification system based primarily on LP.
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.
Appeared in Proceedings of the Fourth International Conference,
CAV'92. LNCS 663, 44-55.
Postscript -
DVI -
LaTeX
TLA Notes
A collection of rough, half-baked notes that
still seem relevant, including
ones sent to an old TLA mailing list.