Abstract
We propose a methodology for the specification, verification, and design of hybrid systems. The methodology consists of the computational model of Concrete Phase Transition Systems (cptss), the specification language of Hybrid Temporal Logic (htl), the graphical system description language of Hybrid Automata, and a proof system for verifying that hybrid automata satisfy their HTL specifications.
The novelty of the approach lies in the continuous-time logic, which allows specification of both point-based and interval-based properties (i.e., properties which describe changes over an interval) and provides direct references to derivatives of variables, and in the proof system that supports verification of point-based and interval-based properties. The proof rules demonstrate that sound and convenient induction rules can be established for continuous-time logics. The proof rules are illustrated on several examples.
Supported in part by the National Science Foundation under grants CCR-92-23226 and CCR-9200794, by the Defense Advanced Research Projects Agency under grants NAG2-703 and NAG2-892, by the United States Air Force Office of Scientific Research under contracts F49620-93-1-0139 and F49620-93-1-0056, and by the European Community ESPRIT Basic Research Action Project 6021 (REACT).
Supported in part by a National Science Foundation Graduate Research Fellowship.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
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.
Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40:269–276, 1991.
Z. Chaochen, A.P. Ravn, and C.A.R. Hoare. An Extended Duration Calculus for Hybrid Real-Time Systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, Lecture Notes in Computer Science 736, pages 36–59. Springer-Verlag, 1993.
D. Harel, D. Kozen, and R. Parikh. Process Logic: Expressiveness, Decidability, Completeness. J. Comp. Sys. Sci., 25:144–170, 1982.
T.A. Henzinger, Z. Manna, and A. Pnueli. Towards Refining Temporal Specifications into Hybrid Systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, Lecture Notes in Computer Science 736, pages 60–76. Springer-Verlag, 1993.
O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 447–484. Springer-Verlag, 1992.
B. Moszkowski. A temporal logic for multi-level reasoning about hardware. IEEE Computer, 18(2):10–19, 1985.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1991.
Z. Manna and A. Pnueli. Models for reactivity. Acta Informatica, 30:609–678, 1993.
X. Nicollin, J. Sifakis, and S. Yovine. From ATP to timed graphs and hybrid systems. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 549–572. Springer-Verlag, 1992.
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, 1993.
F.B. Schneider. Real-time, reliable systems project. Proceedings of the ONR Kickoff Workshop for the Foundations of Real-time Computing Research Initiative, pages 28–32, Office of Naval Research, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kapur, A., Henzinger, T.A., Manna, Z., Pnueli, A. (1994). Proving safety properties of hybrid systems. 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_177
Download citation
DOI: https://doi.org/10.1007/3-540-58468-4_177
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