|
3807
|
1 |
<HTML><HEAD><TITLE>HOL/TLA/README</TITLE></HEAD><BODY bgcolor="white">
|
|
|
2 |
|
|
|
3 |
<H3>TLA: A formalization of TLA in HOL</H3>
|
|
|
4 |
|
|
|
5 |
Author: Stephan Merz<BR>
|
|
|
6 |
Copyright 1997 Universität München<P>
|
|
|
7 |
|
|
|
8 |
The distribution contains a representation of Lamport's
|
|
|
9 |
<A HREF="http://www.research.digital.com/SRC/personal/Leslie_Lamport/tla/tla.html">
|
|
|
10 |
Temporal Logic of Actions</A>
|
|
|
11 |
in Isabelle/HOL.
|
|
|
12 |
|
|
|
13 |
<p>
|
|
|
14 |
|
|
|
15 |
The encoding is mainly oriented towards practical verification
|
|
3849
|
16 |
examples. It does not contain a formalization of TLA's semantics,
|
|
|
17 |
although it could be an interesting exercise to add such a formalization
|
|
|
18 |
to the existing representation. Instead, it is based on a
|
|
|
19 |
<A HREF="http://www4.informatik.tu-muenchen.de/~merz/papers/ptla.ps">complete axiomatization</A>
|
|
|
20 |
of the "raw" (stuttering-sensitive) variant of propositional TLA.
|
|
|
21 |
There is also a
|
|
|
22 |
<A HREF="http://www4.informatik.tu-muenchen.de/~merz/papers/IsaTLADesign.ps">design note</A>
|
|
|
23 |
that explains the basic setup and use of the prover.
|
|
3807
|
24 |
|
|
|
25 |
<p>
|
|
|
26 |
|
|
|
27 |
The distribution includes the following examples:
|
|
|
28 |
<UL>
|
|
|
29 |
<li> a verification of Lamport's <quote>increment</quote> example
|
|
|
30 |
(subdirectory inc),<P>
|
|
|
31 |
|
|
|
32 |
<li> a proof that two buffers in a row implement a single buffer
|
|
|
33 |
(subdirectory buffer), and<P>
|
|
|
34 |
|
|
|
35 |
<li> the verification of Broy and Lamport's RPC-Memory example. For details see:<BR>
|
|
|
36 |
|
|
|
37 |
Martín Abadi, Leslie Lamport, and Stephan Merz:
|
|
|
38 |
<A HREF="http://www4.informatik.tu-muenchen.de/~merz/papers/RPCMemory.html">
|
|
|
39 |
A TLA Solution to the RPC-Memory Specification Problem</A>.
|
|
|
40 |
In: <i>Formal System Specification</i>, LNCS 1169, 1996, 21-69.
|
|
|
41 |
</UL>
|
|
|
42 |
|
|
|
43 |
If you use Isabelle/TLA and have any comments, suggestions or contributions,
|
|
|
44 |
please contact <A HREF="mailto:merz@informatik.uni-muenchen.de">Stephan Merz</A>.
|
|
|
45 |
|
|
|
46 |
</BODY></HTML>
|