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