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.