I/O automata in Isabelle/HOL
| Author(s) : | Konrad Slind Tobias Nipkow, |
| Publisher : | N/A |
| Publication Date : | 1995 |
| ISSN : | N/A |
| Abstract : | Abstract. 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. 1, |