Verification of an audio control protocol

Autor:	Doeko J.B. Bosscher, Frits W. Vaandrager, Indra Polak
Rok vydání:	1994
Předmět:	Language Of Temporal Ordering Specification Correctness Computer science Programming language Hybrid system Formal specification Program derivation Formal methods computer.software_genre Formal verification computer Protocol (object-oriented programming) Automaton
Zdroj:	Lecture Notes in Computer Science ISBN: 9783540584681 FTRTFT
DOI:	10.1007/3-540-58468-4_165
Popis:	We analyze a simple version of a protocol developed by Philips for the physical layer of an interface bus that connects the various devices of some stereo equipment (tuner, CD player,...). The protocol, which uses Manchester encoding, has to deal with a significant uncertainty in the timing of events, due to both hardware and software constraints. We present a formal specification of the protocol, and a proof of correctness for the case where the tolerance of the clocks used within the system is less than 1/17. A counterexample shows that the protocol fails for tolerances greater than or equal to this value. The verification is carried out using a model of linear hybrid systems, which is similar to the phase transition system model of Manna and Pnueli, and the model of linear hybrid automata of Alur, Henzinger and Ho. The semantics of linear hybrid systems is defined via a translation to the timed I/O automata model of Lynch and Vaandrager.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::52c515cd8c4c522b66a326ce6969b636 https://doi.org/10.1007/3-540-58468-4_165 Zobrazit plný text záznamu