The Dagstuhl RPC-Memory Example:
A TLA Solution

Last modified 9 February 2004
The Dagstuhl RPC-Memory Example is a specification and verification problem written for the Dagstuhl Workshop on Reactive Systems held in Dagstuhl, Germany on 26-30 September, 1994. This page describes a solution using TLA - the Temporal Logic of Actions

The Example

Specification Problem
Manfred Broy and Leslie Lamport
6 August 1994 (5 pages)
Postscript - DVI - LaTeX

The TLA Solution

A TLA Solution to the RPC-Memory Specification Problem
Martín Abadi, Leslie Lamport, and Stephan Merz
16 January 1996
Abstract: We present a complete solution to the Broy-Lamport specification problem. Our specifications are written in TLA+, a formal language based on TLA. We give the high levels of structured proofs and sketch the lower levels, which appear in full elsewhere. [see below] (45 pages, with index)
LaTeX - Postscript - DVI

The Complete Proof

An Isabelle/TLA Proof
A mechanically checked version of the proof written by Stephan Merz in Isabelle/TLA, his encoding of TLA in the higher-order logic of the generic interactive theorem prover Isabelle.

Background

The following provide background on TLA and TLA+. See the TLA home page for more information.
Introduction to TLA
Leslie Lamport
23 July 1994
A short (7-page) introduction to what TLA formulas mean. It provides the TLA background needed to read the Dagstuhl specification.

Specifying Systems
Leslie Lamport
2003
The complete guide to TLA+. The first 83 pages should enable you to understand the TLA+ specifications. (There are minor differences between the current TLA+ syntax and the one used in the example.)

Click here for further information on TLA..
Click here for information on the proof style. .

Workshop Proeceedings

This and other solutions appear in Formal Systems Specification: The RPC-Memory Specification Case Study, edited by Manfred Broy, Stephan Merz, and Katharina Spies. Springer-Verlag Lecture Notes in Computer Science, No. 1169.

Comments on the Workshop

Click here for personal observations about the workshop.


This page can be found by searching the Web for the 26-letter string uidlamportdagstuhlspecprob. Please do not put this string in any document that could wind up on the web--including email messages and Postscript and Word documents. You can refer to it in Web documents as "the string obtained by removing the - from uid-lamportdagstuhlspecprob".