Tools for TLA
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
Digital Equipment Corporation (DEC)
- Systems Research Center (SRC)
April 1990 until March 1993
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