1 <HTML><HEAD><TITLE>HOL/TLA/README</TITLE></HEAD><BODY bgcolor="white"> |
1 <HTML><HEAD><TITLE>HOL/TLA</TITLE></HEAD><BODY> |
2 |
2 |
3 <H3>TLA: A formalization of TLA in HOL</H3> |
3 <H2>TLA: Lamport's Temporal Logic of Actions</H2> |
4 |
4 |
5 Author: Stephan Merz<BR> |
5 <A HREF="http://www.research.digital.com/SRC/personal/Leslie_Lamport/tla/tla.html">TLA</A> |
6 Copyright 1997 Universität München<P> |
6 is a linear-time temporal logic introduced by Leslie Lamport in |
|
7 <EM>The Temporal Logic of Actions</EM> (ACM TOPLAS 16(3), 1994, |
|
8 872-923). Unlike other temporal logics, both systems and properties |
|
9 are represented as logical formulas, and logical connectives such as |
|
10 implication, conjunction, and existential quantification represent |
|
11 structural relations such as refinement, parallel composition, and |
|
12 hiding. TLA has been applied to numerous case studies. |
7 |
13 |
8 The distribution contains a representation of Lamport's |
14 <P>This directory formalizes TLA in Isabelle/HOL, as follows: |
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 |
|
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. |
|
24 |
|
25 <p> |
|
26 |
|
27 The distribution includes the following examples: |
|
28 <UL> |
15 <UL> |
29 <li> a verification of Lamport's <em>increment</em> example |
16 <LI>Theory <A HREF="Intensional.html">Intensional</A> prepares the |
30 (subdirectory inc),<P> |
17 ground by introducing basic syntax for "lifted", possibl-world based |
31 |
18 logics. |
32 <li> a proof that two buffers in a row implement a single buffer |
19 <LI>Theories <A HREF="Stfun.html">Stfun</A> and |
33 (subdirectory buffer), and<P> |
20 <A HREF="Action.html">Action</A> represent the state and transition |
34 |
21 level formulas of TLA, evaluated over single states and pairs of |
35 <li> the verification of Broy and Lamport's RPC-Memory example. For details see:<BR> |
22 states. |
36 |
23 <LI>Theory <A HREF="Init.html">Init</A> introduces temporal logic |
37 Martín Abadi, Leslie Lamport, and Stephan Merz: |
24 and defines conversion functions from nontemporal to temporal |
38 <A HREF="http://www4.informatik.tu-muenchen.de/~merz/papers/RPCMemory.html"> |
25 formulas. |
39 A TLA Solution to the RPC-Memory Specification Problem</A>. |
26 <LI>Theory <A HREF="TLA.html">TLA</A> axiomatizes proper temporal |
40 In: <i>Formal System Specification</i>, LNCS 1169, 1996, 21-69. |
27 logic. |
41 </UL> |
28 </UL> |
42 |
29 |
43 If you use Isabelle/TLA and have any comments, suggestions or contributions, |
30 Please consult the |
44 please contact <A HREF="mailto:merz@informatik.uni-muenchen.de">Stephan Merz</A>. |
31 <A HREF="http://www4.in.tum.de/~merz/papers/IsaTLADesign.ps">design notes</A> |
|
32 for further information regarding the setup and use of this encoding |
|
33 of TLA. |
45 |
34 |
|
35 <P> |
|
36 The theories are accompanied by a small number of examples: |
|
37 <UL> |
|
38 <LI><A HREF="Inc/index.html">Inc</A>: Lamport's <EM>increment</EM> |
|
39 example, a standard TLA benchmark, illustrates an elementary TLA |
|
40 proof. |
|
41 <LI><A HREF="Buffer/index.html">Buffer</A>: a proof that two buffers |
|
42 in a row implement a single buffer, uses a simple refinement |
|
43 mapping. |
|
44 <LI><A HREF="Memory/index.html">Memory</A>: a verification of (the |
|
45 untimed part of) Broy and Lamport's <em>RPC-Memory</em> case study, |
|
46 more fully explained in LNCS 1169 (the |
|
47 <A HREF="http://www4.in.tum.de/~merz/papers/RPCMemory.html">TLA |
|
48 solution</A> is available separately). |
|
49 </UL> |
|
50 |
|
51 <HR> |
|
52 |
|
53 <ADDRESS> |
|
54 <A HREF="merz@informatik.uni-muenchen.de">Stephan Merz</A> |
|
55 </ADDRESS> |
|
56 <!-- hhmts start --> |
|
57 Last modified: Mon Jan 25 14:06:43 MET 1999 |
|
58 <!-- hhmts end --> |
46 </BODY></HTML> |
59 </BODY></HTML> |