I/O Automata in Isabelle/HOL

Tobias Nipkow, Konrad Slind

We have embedded the meta-theory of I/O automata, a model for describing and reasoning about distributed systems, in Isabelle's version of higher order logic. On top of that, we have specified and verified a recent network transmission protocol which achieves reliable communication using single-bit-header packets over a medium which may reorder packets arbitrarily.

Postscript SpringerLink

BibTeX:

@inproceedings{Nipkow-Slind-TYPES95,author={Tobias Nipkow and Konrad Slind},
title={{I/O} Automata in {Isabelle/HOL}},
booktitle={Types for Proofs and Programs},
editor={P. Dybjer and B. Nordstr\"om and J. Smith},
publisher=Springer,series=LNCS,volume=996,year=1995,pages={101--119}}

The above model of I/O-Automata is superseded by the work of Müller and Nipkow.