Automated analysis of an audio control protocol

  • Pei -Hsin Ho
  • Howard Wong-Toi
Session 11: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)


We show how HyTech, a symbolic model checker for linear hybrid systems, can be used to analyze an audio control protocol. This protocol [BPV94] was first verified by Bosscher et al. without computer support. In this paper, we demonstrate that algorithmic methods can not only verify the protocol, but can also automatically synthesize the bound on the maximum clock drift, and suggest design modification for a more robust protocol. We believe the techniques we used — finite state encodings, automata transformations, strengthening of specifications — provide insight to the practictioner interested in modeling and analyzing similar real-world applications.


Time Slot Error Tolerance Hybrid Automaton State Predicate Symbolic Model Checker 
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.


  1. [ACHH93]
    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 R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, Lecture Notes in Computer Science 736, pages 209–229. Springer-Verlag, 1993.Google Scholar
  2. [AHH93]
    R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. In Proceedings of the 14th Annual Real-time Systems Symposium, pages 2–11. IEEE Computer Society Press, 1993.Google Scholar
  3. [AHV93]
    R. Alur, T.A. Henzinger, and M.Y. Vardi. Parametric real-time reasoning. In Proceedings of the 25th Annual Symposium on Theory of Computing, pages 592–601. ACM Press, 1993.Google Scholar
  4. [BPV94]
    D. Bosscher, I. Polak, and F. Vaandrager. Verification of an audio-control protocol. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, FTRTFT 94: Formal Techniques in Real-time and Fault-tolerant Systems, Lecture Notes in Computer Science 863, pages 170–192. Springer-Verlag, 1994.Google Scholar
  5. [CHT8]
    P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the Fifth Annual Symposium on Principles of Programming Languages. ACM Press, 1978.Google Scholar
  6. [Hal93]
    N. Halbwachs. Delay analysis in synchronous programs. In C. Courcoubetis, editor, CAV 93: Computer-aided Verification, Lecture Notes in Computer Science 697, pages 333–346. Springer-Verlag, 1993.Google Scholar
  7. [HH95]
    T.A. Henzinger and P.-H. Ho. HyTech: The Cornell Hybrid Technology Tool. To appear, 1995.Google Scholar
  8. [HRP94]
    N. Halbwachs, P. Raymond, and Y.-E. Proy. Verification of linear hybrid systems by means of convex approximation. In Proceedings of the First Static Analysis Symposium, 1994.Google Scholar
  9. [LV92]
    N.A. Lynch and F. Vaandrager. Action transducers and timed automata. In R.J. Cleaveland, editor, CONCUR 92: Theories of Concurrency, Lecture Notes in Computer Science 630, pages 436–455. Springer-Verlag, 1992.Google Scholar
  10. [OSY94]
    A. Olivero, J. Sifakis, and S. Yovine. Using abstractions for the verification of linear hybrid systems. In D.L. Dill, editor, CAV 94: Computer-aided Verification, Lecture Notes in Computer Science 818, pages 81–94. Springer-Verlag, 1994.Google Scholar
  11. [WT94]
    Howard Wong-Toi. Symbolic Approximations for Verifying Real-Time Systems. PhD thesis, Department of Computer Science, Stanford University, CA, December 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Pei -Hsin Ho
    • 1
  • Howard Wong-Toi
    • 1
  1. 1.Computer Science DepartmentCornell UniversityIthaca

Personalised recommendations