Proof-Checking a Data Link Protocol

Abstract. A data link protocol developed and used by Philips Electronics is modeled and veri ed using I/O automata theory. Correctness is computer-checked with the Coq proof development system. Key words: Communication Protocols, I/O Automata, Proof-Checking, Protocol Veri cation, Type Theory.

• Type: Conference
• Year: 1993
• Where: TYPES
• Authors: Leen Helmink, M. P. A. Sellink, Frits W. Vaandrager
• Keywords: Formal Methods, I/O Automata, I/O Automata Theory, Protocol Veri Cation, TYPES 1993