Proof-Checking a Data Link Protocol
Publication date
1994-03
Authors
Helmink, L.
Sellink, M.P.A.
Vaandrager, F.W.
Editors
Advisors
Supervisors
DOI
Document Type
Preprint
Metadata
Show full item recordCollections
License
Abstract
A data link protocol developed and used by Philips Electronics is modeled and verified using I/O automata theory. Correctness
is computer-checked with the Coq proof development system.
Keywords
Communication Protocols, I/O Automata, Proof-Checking, Protocol Verification, Type Theory