A Proof-checked Verification of a Real-Time Communication Protocol

Abstract

We present an analysis of a protocol developed by Philips to connect several components of an audio-system. The verification of the protocol is carried out using the timed I/O-automata model of Lynch and Vaandrager. The verification has been partially proof-checked with the interactive proof construction program Coq. The proof-checking revealed an error in the correctness proof (not in the protocol!).