Department of Informatics

TU München - Fakultät für Informatik
Chair IV: Software & Systems Engineering

PDF-Datei  A TLA Solution to the RPC-Memory Specification problem


Author:Martín Abadi, Leslie Lamport, Stephan Merz
Conference:Formal Systems Specification: The RPC-Memory Specification Case Study. Lecture Notes in Computer Science 1169
Editor:M. Broy, S. Merz, K. Spies
Pages:21 - 66
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 will appear in full elsewhere.

(c) 1999-2006 - Lehrstuhl Software & Systems Engineering
Sitemap |  Contact