Abstract
We propose a formal framework for designing hybrid systems by stepwise refinement. Starting with a specification in hybrid temporal logic, we make successively more transitions explicit until we obtain an executable system.
This research was supported in part by the National Science Foundation under grants CCR-92-00794 and CCR-92-23226, by the Defense Advanced Research Projects Agency under contract NAG2-703, by the United States Air Force Office of Scientific Research under contracts F49620-93-1-0056 and F49620-93-1-0139, and by the European Community ESPRIT Basic Research Action Project 6021 (REACT).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. Composing specifications. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, Lecture Notes in Computer Science 430. Springer-Verlag, 1990.
R. Alur and T.A. Henzinger. Logics and models of real time: a survey. 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 74–106. Springer-Verlag, 1992.
Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40:269–276, 1992.
T.A. Henzinger. Sooner is safer than later. Information Processing Letters, 43:135–141, 1992.
T.A. Henzinger, Z. Manna, and A. Pnueli. Timed transition 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 226–251. Springer-Verlag, 1992.
T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science, pages 394–406. IEEE Computer Society Press, 1992.
L. Lamport and M. Abadi. An old-fashioned recipe for real time. 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 1–27. Springer-Verlag, 1992.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henzinger, T.A., Manna, Z., Pnueli, A. (1993). Towards refining temporal specifications into hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds) Hybrid Systems. HS HS 1992 1991. Lecture Notes in Computer Science, vol 736. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57318-6_24
Download citation
DOI: https://doi.org/10.1007/3-540-57318-6_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57318-0
Online ISBN: 978-3-540-48060-0
eBook Packages: Springer Book Archive