Skip to main content
SpringerLink
Log in

Verification of an audio control protocol

  • Conference paper
  • First Online:
Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 1994, ProCoS 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 863))

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.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi and L. Lamport. An old-fashioned recipe for real time. In de Bakker et al. [6], pages 1–27.

    Google Scholar 

  2. 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.

    Google Scholar 

  3. 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.

    Google Scholar 

  4. 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.

    Google Scholar 

  5. D.J.B. Bosscher, I. Polak, and F.W. Vaandrager. Verification of an audio control protocol. Report CS-R94XX, CWI, Amsterdam, 1994. To appear.

    Google Scholar 

  6. 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.

    Google Scholar 

  7. 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.

    Google Scholar 

  8. 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.

    Google Scholar 

  9. W.O.D. Griffioen. Analysis of an Audio Control Protocol wi th Bus Collision. Master thesis, Programming Research Group, University of Amsterdam, 1994.

    Google Scholar 

  10. 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.

    Google Scholar 

  11. 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.

    Google Scholar 

  12. 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.

    Google Scholar 

  13. L. Lamport. A temporal logic of actions. Research Report 79, Digital Equipment Corporation, Systems Research Center, December 1991.

    Google Scholar 

  14. L. Lamport. Hybrid systems in TLA+. In Grossman et al. [10], pages 77–102.

    Google Scholar 

  15. 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.

    Google Scholar 

  16. N.A. Lynch, M. Merritt, W. Weihl, and A. Fekete. Atomic Transactions. Morgan Kaufmann Publishers, 1994.

    Google Scholar 

  17. 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.

    Google Scholar 

  18. N.A. Lynch and F.W. Vaandrager. Forward and backward simulations — part I: Untimed systems. Report CS-R9313, CWI, Amsterdam, March 1993.

    Google Scholar 

  19. N.A. Lynch and F.W. Vaandrager. Forward and backward simulations — part II: Timing-based systems. Report CS-R9314, CWI, Amsterdam, March 1993.

    Google Scholar 

  20. O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In de Bakker et al. [6], pages 447–484.

    Google Scholar 

  21. Z. Manna and A. Pnueli. Verifying hybrid systems. In Grossman et al. [10], pages 4–35.

    Google Scholar 

  22. 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.

    Google Scholar 

  23. 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.

    Google Scholar 

  24. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):319–340, 1976.

    Google Scholar 

  25. 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.

    Google Scholar 

  26. R.S. Roden. Digital Communication Systems Design. Prentice Hall, 1988.

    Google Scholar 

  27. 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.

    Google Scholar 

  28. 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.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, P.O. Box 94079, 1090, GB Amsterdam, The Netherlands

    Doeko Bosscher & Frits Vaandrager

  2. Department of Philosophy, Utrecht University, P.O. Box 80126, 3508, TC Utrecht, The Netherlands

    Indra Polak

  3. Programming Research Group, University of Amsterdam, Kruislaan 403, 1098, SJ Amsterdam, The Netherlands

    Frits Vaandrager

Authors
  1. Doeko Bosscher
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Indra Polak
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Frits Vaandrager
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Hans Langmaack Willem-Paul de Roever Jan Vytopil

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation