Abstract
This paper is addressed to potential users of HyTech, the Cornell Hybrid Technology Tool, an automatic tool for analyzing hybrid systems. We review the formal technologies that have been incorporated into HyTech, and we illustrate the use of HyTech with three nontrivial case studies.
This research was supported in part by the National Science Foundation under grant CCR-9200794, by the Air Force Office of Scientific Research under contract F49620-93-1-0056, by the Office of Naval Research under YIP grant N00014-95-1-0520, and by the Defense Advanced Research Projects Agency under grant NAG2-892.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
[ACH+95] R. Alur, C. Coucoubetis, 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.
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.
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.
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.
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.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, California, 1977. ACM Press.
P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In PLILP, Lecture Notes in Computer Science 631, pages 269–295. Springer-Verlag, 1992.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
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.
J.C. Corbett. Modeling and analysis of real-time Ada tasking programs. In Proceedings of the 15th Annual Real-time Systems Symposium. IEEE Computer Society Press, 1994.
D.L. Dill and H. Wong-Toi. Verification of real-time systems by successive over-and underapproximation. In CAV 95: Computer-aided Verification, Lecture Notes in Computer Science. Springer-Verlag, 1995.
C. Daws and S. Yovine. Verification of multirate timed automata with KRONOS: two examples. Technical Report Spectre-95-06, VERIMAG, April 1995.
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.
T.A. Henzinger and P.-H. Ho. Algorithmic analysis of nonlinear hybrid systems. In CAV 95: Computer-aided Verification, Lecture Notes in Computer Science. Springer-Verlag, 1995.
T.A. Henzinger and P.-H. Ho. A note on abstract-interpretation strategies for hybrid automata. This volume, 1995.
T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTecH: The next generation. Submitted, 1995.
N. Halbwachs, P. Raymond, and Y.-E. Proy. Verification of linear hybrid systems by means of convex approximation. In B. LeCharlier, editor, International Symposium on Static Analysis, SAS'94, Lecture Notes in Computer Science 864, Namur (belgium), September 1994. Springer-Verlag.
P.-H. Ho and H. Wong-Toi. Automated analysis of an audio control protocol. In CAV 95: Computer-aided Verification, Lecture Notes in Computer Science. Springer-Verlag, 1995.
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.
N.A. Lynch and F. Vaandrager. Forward and backward simulations, part ii: timing-based systems. Technical Report CS-R9314, CWI, Amsterdam, 1993.
X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An approach to the description and analysis 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 149–178. Springer-Verlag, 1993.
A. Puri and P. Varaiya. Verification of hybrid systems using abstractions. This volume, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henzinger, T.A., Ho, PH. (1995). HyTech: The Cornell Hybrid Technology Tool. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds) Hybrid Systems II. HS 1994. Lecture Notes in Computer Science, vol 999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60472-3_14
Download citation
DOI: https://doi.org/10.1007/3-540-60472-3_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60472-3
Online ISBN: 978-3-540-47519-4
eBook Packages: Springer Book Archive