Advertisement

HyTech: A model checker for hybrid systems

  • Thomas A. Henzinger
  • Pei-Hsin Ho
  • Howard Wong-Toi
Tool Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)

Abstract

A hybrid system consists of a collection of digital programs that interact with each other and with an analog environment. Examples of hybrid systems include medical equipment, manufacturing controllers, automotive controllers, and robots. The formal analysis of the mixed digital-analog nature of these systems requires a model that incorporates the discrete behavior of computer programs with the continuous behavior of environment variables, such as temperature and pressure. Hybrid automata capture both types of behavior by combining finite automata with differential inclusions (i.e. differential inequalities). HyTech is a symbolic model checker for linear hybrid automata, an expressive, yet automatically analyzable, subclass of hybrid automata. A key feature of HyTech is its ability to perform parametric analysis, i.e. to determine the values of design parameters for which a linear hybrid automaton satisfies a temporal requirement.

Keywords

Hybrid System Differential Inclusion Finite Automaton Hybrid Automaton Symbolic Model Check 
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.

References

  1. 1.
    R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.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 Hybrid Systems I, LNCS 736, pp. 209–229. Springer, 1993.Google Scholar
  3. 3.
    R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.Google Scholar
  4. 4.
    R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Trans. Software Engineering, 22:181–201, 1996.Google Scholar
  5. 5.
    R. Alur, T.A. Henzinger, and E.D. Sontag, eds. Hybrid Systems III: Verification and Control. LNCS 1066. Springer, 1996.Google Scholar
  6. 6.
    R. Alur, T.A. Henzinger, and M.Y. Vardi. Parametric real-time reasoning. In Proc. 25th ACM Symp. Theory of Computing, pp. 592–601, 1993.Google Scholar
  7. 7.
    R. Alur and R.P. Kurshan. Timing analysis in Cospan. In Hybrid Systems III, LNCS 1066, pp. 220–231. Springer, 1996.Google Scholar
  8. 8.
    P. Antsaklis, A. Nerode, W. Kohn, and S. Sastry, eds. Hybrid Systems II. LNCS 999. Springer, 1995.Google Scholar
  9. 9.
    J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi. UppAal: a tool-suite for automatic verification of real-time systems. In Hybrid Systems III, LNCS 1066, pp. 232–243. Springer, 1996.Google Scholar
  10. 10.
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142–170, 1992.Google Scholar
  11. 11.
    E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, LNCS 131. Springer, 1981.Google Scholar
  12. 12.
    J. C. Corbett. Timing analysis of Ada tasking programs. IEEE Trans. Software Engineering, 22:461–483, 1996.Google Scholar
  13. 13.
    P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. 5th ACM Symp. Principles of Programming Languages, pp. 84–97, 1978.Google Scholar
  14. 14.
    C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool Kronos. In Hybrid Systems III, LNCS 1066, pp. 208–219. Springer, 1996.Google Scholar
  15. 15.
    J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, eds. Real Time: Theory in Practice. LNCS 600. Springer, 1992.Google Scholar
  16. 16.
    A. Deshpande, A. Göllü, and L. Semenzato. The Shift programming language and runtime system for dynamic networks of hybrid automata. PATH report, http://www-path. eecs.berkeley.edu/shift/doc/ieeshift.ps.gz, 1996.Google Scholar
  17. 17.
    D.L. Dill and H. Wong-Toi. Verification of real-time systems by successive over-and underap-proximation. In Computer-aided Verification, LNCS 939, pp. 409–422. Springer, 1995.Google Scholar
  18. 18.
    R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, eds. Hybrid Systems I. LNCS 736. Springer, 1993.Google Scholar
  19. 19.
    N. Halbwachs, P. Raymond, and Y.-E. Proy. Verification of linear hybrid systems by means of convex approximation. In Static Analysis Symp., LNCS 864, pp. 223–237. Springer, 1994.Google Scholar
  20. 20.
    M.R. Henzinger, T.A. Henzinger, and P.W. Kopke. Computing simulations on finite and infinite graphs. In Proc. 36rd IEEE Symp. Foundations of Computer Science, pp. 453–462, 1995.Google Scholar
  21. 21.
    T.A. Henzinger. Hybrid automata with finite bisimulations. In ICALP: Automata, Languages, and Programming, LNCS 944, pp. 324–335. Springer, 1995.Google Scholar
  22. 22.
    T.A. Henzinger. The theory of hybrid automata. In Proc. 11th IEEE Symp. Logic in Computer Science, pp. 278–292, 1996.Google Scholar
  23. 23.
    T.A. Henzinger and P.-H. Ho. Algorithmic analysis of nonlinear hybrid systems. In Computer-aided Verification, LNCS 939, pp. 225–238. Springer, 1995.Google Scholar
  24. 24.
    T.A. Henzinger and P.-H. Ho. HyTech: The Cornell Hybrid Technology Tool. In Hybrid Systems II, LNCS 999, pp. 265–293. Springer, 1995.Google Scholar
  25. 25.
    T.A. Henzinger and P.-H. Ho. A note on abstract-interpretation strategies for hybrid automata. In Hybrid Systems II, LNCS 999, pp. 252–264. Springer, 1995.Google Scholar
  26. 26.
    T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: the next generation. In Proc. 16th IEEE Real-time Systems Symp., pp. 56–65, 1995.Google Scholar
  27. 27.
    T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. A user guide to HyTech. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1019, pp. 41–71. Springer, 1995.Google Scholar
  28. 28.
    T.A. Henzinger and P.W. Kopke. State equivalences for rectangular hybrid automata. In Concurrency Theory, LNCS 1119, pp. 530–545. Springer, 1996.Google Scholar
  29. 29.
    T.A. Henzinger and P.W. Kopke. Discrete-time control for rectangular hybrid automata. In ICALP: Automata, Languages, and Programming, LNCS. Springer, 1997.Google Scholar
  30. 30.
    T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? In Proc. 27th ACM Symp. Theory of Computing, pp. 373–382, 1995.Google Scholar
  31. 31.
    T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111:193–244, 1994.Google Scholar
  32. 32.
    T.A. Henzinger and H. Wong-Toi. Linear phase-portrait approximations for nonlinear hybrid systems. In Hybrid Systems III, LNCS 1066, pp. 377–388. Springer, 1996.Google Scholar
  33. 33.
    T.A. Henzinger and H. Wong-Toi. Using HyTech to synthesize control parameters for a steam boiler. In Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS 1165, pp. 265–282. Springer, 1996.Google Scholar
  34. 34.
    P.-H. Ho. Automatic Analysis of Hybrid Systems. PhD thesis, Cornell Univ., 1995.Google Scholar
  35. 35.
    P.-H. Ho and H. Wong-Toi. Automated analysis of an audio control protocol. In Computeraided Verification, LNCS 939, pp. 381–394. Springer, 1995.Google Scholar
  36. 36.
    P.W. Kopke. The Theory of Rectangular Hybrid Automata. PhD thesis, Cornell Univ., 1996.Google Scholar
  37. 37.
    S. Nadjm-Tehrani and J.-E. Strömberg. Proving dynamic properties in an aerospace application. In Proc. 16th IEEE Real-time Systems Symp., pp. 2–10, 1995.Google Scholar
  38. 38.
    X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An approach to the description and analysis of hybrid systems. In Hybrid Systems I, LNCS 736, pp. 149–178. Springer, 1993.Google Scholar
  39. 39.
    J. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Symp. on Programming, LNCS 137, pp. 337–351. Springer, 1981.Google Scholar
  40. 40.
    T. Stauner, O. Müller, and M. Fuchs. Using HyTech to verify an automotive control system. In Hybrid and Real-Time Systems, LNCS 1201, pp. 139–153. Springer, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Thomas A. Henzinger
    • 1
  • Pei-Hsin Ho
    • 2
  • Howard Wong-Toi
    • 3
  1. 1.EECS DepartmentUniversity of CaliforniaBerkeley
  2. 2.Strategic CAD LabsIntel CorporationHillsboro
  3. 3.Cadence Berkeley LabsBerkeley

Personalised recommendations