Abstract
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.
The first and third author were supported by Esprit BRA 7166 CONCUR 2.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi and L. Lamport. An old-fashioned recipe for real time. In de Bakker et al. [6], pages 1–27.
R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In Grossman et al. [10], pages 209–229.
R. Alur and D.L. Dill. Automata for modeling real-time systems. In M. Paterson, editor, Proceedings 17 th ICALP, Warwick, volume 443 of Lecture Notes in Computer Science, pages 322–335. Springer-Verlag, July 1990.
R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. In Proceedings of the 14 th Annual IEEE Real-time Systems Symposium, 1993.
D.J.B. Bosscher, I. Polak, and F.W. Vaandrager. Verification of an audio control protocol. Report CS-R94XX, CWI, Amsterdam, 1994. To appear.
J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors. Proceedings REX Workshop on Real-Time: Theory in Practice, Mook, The Netherlands, June 1991, volume 600 of Lecture Notes in Computer Science. Springer-Verlag, 1992.
G. Dowek, A. Felty, H. Herbelin, G.P. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq proof assistant user's guide. Version 5.8. Technical report, INRIA — Rocquencourt, May 1993.
R. Gawlick, R. Segala, J. SØgaard-Andersen, and N.A. Lynch. Liveness in timed and untimed systems. Technical Report MIT/LCS/TR-587, Laboratory for Computer Science, MIT, Cambridge, MA, December 1993. An extended abstract will appear in Proceedings ICALP'94.
W.O.D. Griffioen. Analysis of an Audio Control Protocol wi th Bus Collision. Master thesis, Programming Research Group, University of Amsterdam, 1994.
R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors. Hybrid Systems, volume 736 of Lecture Notes in Computer Science. Springer-Verlag, 1993.
L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. In H. Barendregt and T. Nipkow, editors, Proceedings International Workshop TYPES'93, Nijmegen, The Netherlands, May 1993, number 806 in Lecture Notes in Computer Science, pages 127–165. Springer-Verlag, 1994. Full version available as Report CS-R9420, CWI, Amsterdam, March 1994.
A.S.A. Jeffrey, S.A. Schneider, and F.W. Vaandrager. A comparison of additivity axioms in timed transition systems. Report CS-R9366, CWI, Amsterdam, November 1993.
L. Lamport. A temporal logic of actions. Research Report 79, Digital Equipment Corporation, Systems Research Center, December 1991.
L. Lamport. Hybrid systems in TLA+. In Grossman et al. [10], pages 77–102.
B.W. Lampson, N.A. Lynch, and J.F. SØgaard-Andersen. Correctness of at-most-once message delivery protocols. In Formal Description Techniques VI. North-Holland, 1993.
N.A. Lynch, M. Merritt, W. Weihl, and A. Fekete. Atomic Transactions. Morgan Kaufmann Publishers, 1994.
N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6 th Annual ACM Symposium on Principles of Distributed Computing, pages 137–151, August 1987. A full version is available as MIT Technical Report MIT/LCS/TR-387.
N.A. Lynch and F.W. Vaandrager. Forward and backward simulations — part I: Untimed systems. Report CS-R9313, CWI, Amsterdam, March 1993.
N.A. Lynch and F.W. Vaandrager. Forward and backward simulations — part II: Timing-based systems. Report CS-R9314, CWI, Amsterdam, March 1993.
O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In de Bakker et al. [6], pages 447–484.
Z. Manna and A. Pnueli. Verifying hybrid systems. In Grossman et al. [10], pages 4–35.
J.S. Moore. A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol. Journal of Formal Aspects of Computing Science, 6(1):60–91, 1994.
X. Nicollin and J. Sifakis. An overview and synthesis on timed process algebras. In K.G. Larsen and A. Skou, editors, Proceedings of the 3rd International Workshop on Computer Aided Verification, Aalborg, Denmark, volume 575 of Lecture Notes in Computer Science, pages 376–398. Springer-Verlag, 1992.
S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):319–340, 1976.
A.P. Ravn, H. Rischel, and K.M. Hansen. Specifying and verifying requirements of real-time systems. IEEE Transactions on Software Engineering, 19(1):41–55, January 1993.
R.S. Roden. Digital Communication Systems Design. Prentice Hall, 1988.
F.W. Vaandrager and N.A. Lynch. Action transducers and timed automata. In W.R. Cleaveland, editor, Proceedings CONCUR 92, Stony Brook, NY, USA, volume 630 of Lecture Notes in Computer Science, pages 436–455. Springer-Verlag, 1992.
Wang Yi. Real-time behaviour of asynchronous agents. In J.C.M. Baeten and J.W. Klop, editors, Proceedings CONCUR 90, Amsterdam, volume 458 of Lecture Notes in Computer Science, pages 502–520. Springer-Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bosscher, D., Polak, I., Vaandrager, F. (1994). Verification of an audio control protocol. In: Langmaack, H., de Roever, WP., Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT ProCoS 1994 1994. Lecture Notes in Computer Science, vol 863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58468-4_165
Download citation
DOI: https://doi.org/10.1007/3-540-58468-4_165
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58468-1
Online ISBN: 978-3-540-48984-9
eBook Packages: Springer Book Archive