Tools for TLA

Project description

This project dealt with the investigation of tool-support for the application of TLA (Temporal Logic of Actions, L. Lamport 1989) and the corresponding specification language TLA+. In the CD-part of the project (construction and design) more conventional tools - specification editor / browser, specification interpreter, animation of specifications - have been under study. The AV-part (analysis and verification) investigates the different possibilities for the support of verification tasks - logical proofs by means of automated theorem provers, automated reachability analysis tools, and model checkers for finite state systems.

Analysis and Verification (AV)

Construction and Design (CD)


An extra page lists the projects publications, papers, and reports externally available.

Project Partner

Digital Equipment Corporation (DEC)
- Systems Research Center (SRC)

Project Duration

April 1990 until March 1993

Project Results

A software list gives a short summary about tools build and made available.


References to TLA

You will find references to TLA, other TLA users, tools, and repositories on an extra page.

Peter Herrmann, January 21, 1998
Informatik IV, Uni Dortmund