Advertisement

Verification of an audio control protocol

  • Doeko Bosscher
  • Indra Polak
  • Frits Vaandrager
Conference paper
Part of the Lecture Notes in Computer Science book series (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.

Keywords

Hybrid System Input Action Reachable State Label Transition System Constant Symbol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 13.
    L. Lamport. A temporal logic of actions. Research Report 79, Digital Equipment Corporation, Systems Research Center, December 1991.Google Scholar
  14. 14.
    L. Lamport. Hybrid systems in TLA+. In Grossman et al. [10], pages 77–102.Google Scholar
  15. 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. 16.
    N.A. Lynch, M. Merritt, W. Weihl, and A. Fekete. Atomic Transactions. Morgan Kaufmann Publishers, 1994.Google Scholar
  17. 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. 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. 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. 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. 21.
    Z. Manna and A. Pnueli. Verifying hybrid systems. In Grossman et al. [10], pages 4–35.Google Scholar
  22. 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. 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. 24.
    S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):319–340, 1976.Google Scholar
  25. 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. 26.
    R.S. Roden. Digital Communication Systems Design. Prentice Hall, 1988.Google Scholar
  27. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Doeko Bosscher
    • 1
  • Indra Polak
    • 2
  • Frits Vaandrager
    • 1
    • 3
  1. 1.CWIGB AmsterdamThe Netherlands
  2. 2.Department of PhilosophyUtrecht UniversityTC UtrechtThe Netherlands
  3. 3.Programming Research GroupUniversity of AmsterdamSJ AmsterdamThe Netherlands

Personalised recommendations