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)
-
Publications
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.
Contact
-
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