src/HOLCF/IOA/README.html
author mueller
Wed Apr 30 11:20:15 1997 +0200 (1997-04-30)
changeset 3071 981258186b71
child 3279 815ef5848324
permissions -rw-r--r--
New meta theory for IOA based on HOLCF.
     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&auml;t M&uuml;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&uuml;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&uuml;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