Abstract
Functional specifications have been used to specify and verify designs of a number of reactive, discrete systems. In this paper we extend this specification style to deal with real-time and hybrid systems. As mathematical foundation we employ Banach's fixed point theory in metric spaces. The goal is to show that the theory used for discrete functional specifications smoothly carries over to real-time and hybrid systems. An example of a thermostat specification illustrates the method.
This work is partially sponsored by the German Federal Ministry of Education and Research (BMBF) as part of the compound project “KorSys” and by BMW (Bayerische Motoren Werke AG).
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
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(1):3–34, 1995.
P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry. Hybrid Systems II, volume 999. Springer Verlag, 1995. Lecture Notes in Computer Science.
M. Broy, F. Dederichs, C. Dendorfer, M. Fuchs, T. F. Gritzner, and R. Weber. The Design of Distributed Systems: An Introduction to Focus — Revised Version. Technical Report TUM-I9202-2, Technische Universität München, Fakultät für Informatik, 80290 München, Germany, 1993.
M. Broy. Interaction Refinement — The Easy Way. In M. Broy, editor, Program Design Calculi, volume 118 of NATO ASI Series F: Computer and System Sciences. Springer, 1993.
R. Engelking. General Topology. PWN — Polish Scientific Publishers, 1977.
R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel. Hybrid Systems, volume 736. Springer Verlag, 1993. Lecture Notes in Computer Science.
R. Grosu and K. Stølen. A Model for Mobile Point-to-Point Dataflow Networks without Channel Sharing. In Proc. of the 5th International Conference on Algebraic Methodology and Software Technology AMAST'96, Munich, volume 1101 of Lecture Notes in Computer Science, pages 513–519, 1996. Also available as Technical Report TUM-I9527, Technische Universität München.
L. Lamport. Hybrid Systems in TLA+. In R.L. Grossman et al., editor, [GNRR93], 1993.
N. Lynch, R. Segala, F. Vaandrager, and H.B. Weinberg. Hybrid I/O automata. Technical Report CS-R9578, CWI, Computer Science Department, Amsterdam, 1995. Available under http://www.cs.kun.nl/∼fvaan/.
Z. Manna and A. Pnueli. Verifying Hybrid Systems. In Grossman et al., editor, [GNRR93], 1993.
M.D. Mesarovic and Y. Takahara. General Systems Theory: Mathematical Foundations, volume 113. Academic Press, 1975. Mathematics in Science and Engineering.
D. Scott and C. Gunter. Semantic Domains and Denotational Semantics. In Handbook of Theoretical Computer Science, chapter 12, pages 633–674. Elsevier Science Publisher, 1990.
W. A. Sutherland. Introduction to metric and topological spaces. Claredon Press-Oxford, 1975.
G. Winskel. The Formal Semantics of Programming Languages. The MIT Press, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller, O., Scholz, P. (1997). Functional specification of real-time and hybrid systems. In: Maler, O. (eds) Hybrid and Real-Time Systems. HART 1997. Lecture Notes in Computer Science, vol 1201. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014732
Download citation
DOI: https://doi.org/10.1007/BFb0014732
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62600-8
Online ISBN: 978-3-540-68330-8
eBook Packages: Springer Book Archive