author wenzelm
Wed, 08 Oct 1997 11:50:33 +0200
changeset 3807 82a99b090d9d
child 3849 3ea10bfd329d
permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;


<H3>TLA: A formalization of TLA in HOL</H3>

Author:     Stephan Merz<BR>
Copyright   1997 Universit&auml;t M&uuml;nchen<P>

The distribution contains a representation of Lamport's
<A HREF="">
Temporal Logic of Actions</A>
in Isabelle/HOL.


The encoding is mainly oriented towards practical verification
examples. It does not contain a formalization of TLA's semantics;
instead, it is based on a 
<A HREF="doc/PTLA.dvi">complete axiomatization</A> of the "raw"
(stuttering-sensitive) variant of propositional TLA. It is
accompanied by a
<A HREF="doc/design.dvi">design note</A> that explains the basic 
setup and use of the prover.


The distribution includes the following examples:
  <li> a verification of Lamport's <quote>increment</quote> example
  (subdirectory inc),<P>

  <li> a proof that two buffers in a row implement a single buffer
  (subdirectory buffer), and<P>

   <li> the verification of Broy and Lamport's RPC-Memory example. For details see:<BR>

        Mart&iacute;n Abadi, Leslie Lamport, and Stephan Merz: 
        <A HREF="">
        A TLA Solution to the RPC-Memory Specification Problem</A>.
        In: <i>Formal System Specification</i>, LNCS 1169, 1996, 21-69.

If you use Isabelle/TLA and have any comments, suggestions or contributions,
please contact <A HREF="">Stephan Merz</A>.