Publications and Papers

'Tools for TLA based specifications' project
Computer Networks and Distributed Systems Group
Department of Computer Science, University of Dortmund, Germany

Research Reports

These reports are also available on anonymous FTP ( under /pub/ls04-info/research-reports/FB*) and on paper by request to the appropriate author.

Peter Herrmann, Heiko Krumm: Report on Analysis and Verification Techniques. Forschungsbericht/Research Report 485/1993, Universität Dortmund, Fachbereich Informatik, 1993

(Table of Contents/Introduction or full text, 58 pages, 147KB compressed postscript )

Ulrich Eickhoff, Peter Herrmann, Heiko Krumm: Theorem prover based verification of TLA systems. Forschungsbericht/Research Report 492/1993, Universität Dortmund, Fachbereich Informatik, May 1993

(Abstract or full text, 16 pages, 112KB compressed postscript )

P. Herrmann, Th. Kraatz, H. Krumm, M. Stange: Automated Verification of Refinements of Concurrent and Distributed Systems. Forschungsbericht/Research Report 541/1994, Universität Dortmund, Fachbereich Informatik, March 1994

(Abstract or full text, 17 pages, 94KB compressed postscript )

Contribution to Workshops (german language)

H. Krumm: Werkzeugunterstützte Einarbeitung in formale Protokollspezifikationen.
1. Fachgespräch der GI/ITG Fachgruppe 'Formale Beschreibungstechniken für verteilte Systeme',
Darmstadt, Juni 1991

A. Mester: Spezifikation verteilter Systeme mit TLA(+) (Inhaltsangabe),
P. Herrmann: Rechnergestützte Verifikation verteilter Systeme .
2. Fachgespräch der GI/ITG Fachgruppe 'Formale Beschreibungstechniken für verteilte Systeme',
Magdeburg, Juni 1992

A. Mester, H.Krumm: Animation von TLA Spezifikationen (Inhaltsangabe),
P. Herrmann, H. Krumm: Strukturierte Protokollverifikation in TLA (Inhaltsangabe).
3. Fachgespräch der GI/ITG Fachgruppe 'Formale Beschreibungstechniken für verteilte Systeme',
München, Juni 1993

A. Mester, H. Krumm: Entwurf verteilter Anwendungen mit TLA.
in: Tagungsband zum GI/ITG Arbeitstreffen 'Entwurf und Management verteilter Anwendungssysteme'
Frankfurt, 1993
(Kurzfassung oder Volltext, 12 Seiten, 85KB compressed postscript )

Technical Papers (available on demand)

Arnulf Mester tTLA+ 1 syntax description. RvS-TLA-92/4, Jan 93 (abstract, full text (compressed dvi))

Rainer Grote, Peter Herrmann, Heiko Krumm Modulare Spezifikationen basierend auf TA Spezifikationen (xTA-Konzept). RvS-TLA-91/5 (abstract, full text)

Peter Herrmann, Arnulf Mester Some experiences with specifying in TLA+. Dok-L07-92/6, Nov 92

Joerg Dickmann, Peter Herrmann: Transition Axioms description for Leif. Dok-TLA-91/7, Apr 91

Peter Herrmann: How to edit TA specifications with Leif and GNU emacs . Dok-TLA-91/8, Apr 91

Peter Herrmann Specification and Verification of the Sliding Window Protocol in TLA . Dok-TLA-92/14, Sep 92

Peter Herrmann The proof of the invariant of the sliding window protocol . Dok-TLA-92/15, Sep 92

Dok-TLA-92/17, Nov 92 eTLA+ - an executable subset of TLA+.

Heiko Krumm Outline of a TLA+-Style . Dok-TLA-93/23, Jul 93

Arnulf Mester, Peter Herrmann: Tools for TLA-based specifications. RvS-TLA-94/35 (compressed dvi-file)

Arnulf Mester, last updated: Apr 10, 1995
Informatik IV, Uni Dortmund