|
1 <HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY> |
|
2 |
|
3 <H3>IOA: A formalization of I/O automata in HOLCF</H3> |
|
4 |
|
5 Author: Olaf Mueller<BR> |
|
6 Copyright 1997 Technische Universität München<P> |
|
7 |
|
8 Version: 1.0<BR> |
|
9 Date: 1.05.97<P> |
|
10 |
|
11 The distribution contains |
|
12 |
|
13 <UL> |
|
14 <li> A semantic model of the meta theory of I/O automata including proofs for the refinement notion |
|
15 and the compositionality of the model. For details see: <BR> |
|
16 Olaf Müller and Tobias Nipkow, |
|
17 <A HREF="http://www4.informatik.tu-muenchen.de/papers/tapsoft_mueller_1997_Conference.html">Traces of I/O Automata in Isabelle/HOLCF</A>. |
|
18 In <i> TAPSOFT'97, Proc. of the 7th International Joint Conference on Theory and Practice of Software Development </i>, LNCS 1224, 1997.<P> |
|
19 |
|
20 <li> A proof of the Alternating Bit Protocol (ABP subdirectory) with unbounded buffers using |
|
21 a combination of Isabelle and a model checker. This case study is performed within the |
|
22 theory of IOA described above. For details see:<BR> |
|
23 Olaf Müller and Tobias Nipkow, |
|
24 <A HREF="http://www4.informatik.tu-muenchen.de/papers/MuellerNipkow_TaAf1995.html">Combining Model Checking and Deduction for I/O Automata </A>. |
|
25 In <i> TACAS'95, Proc. of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems </i>, LNCS 1019, 1995.<P> |
|
26 <li> A proof of a Network Transmission Protocol (NTP subdirectory) using the theory of IOA described above. For details see:<BR> |
|
27 |
|
28 Tobias Nipkow, Konrad Slind. |
|
29 <A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ioa.html> |
|
30 I/O Automata in Isabelle/HOL</A>. In <i>Types for Proofs and Programs</i>, |
|
31 LNCS 996, 1995, 101-119. |
|
32 |
|
33 </UL> |
|
34 |
|
35 </BODY></HTML> |
|
36 |
|
37 |
|
38 |