Abstract
We describe a variant of discrete temporal interval logics which is embedded, and extends the Z notation. The resulting formalism, called DZ, includes the usual set of operators known from interval logics together with a set of operators tailored for the operational description of deterministic process behavior. We apply our approach to the foundation of a combination of Statecharts and Z by giving a translation from a significant subset of Statecharts into DZ.
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. Büssow, R. Geisler, and M.Klar. Spezifikation eingebetteter Steuerungssysteme mit Z und Statecharts. In Tagungsband zur 5. Fachtagung Entwurf komplexer Automatisierung ssysteme. TU Braunschweig, 1997.
Robert Büssow, Heiko Dörr, Robert Geisler, Wolfgang Grieskamp, and Marcus Klar. MSZ — ein Ansatz zur systematischen Verbindung von Z und Statecharts. Technical Report TR 96-32, Technische Universität Berlin, 1996.
Z. Chaochen, C. A. R. Hoare, and A.P Ravn. A calculus of durations. Information Processing Letters, 40(5), 1991.
M. Engel. Specifying real-time systems with Z and the Duration Calculus. In J. Bowen and J. Hall, editors, Z User Workshop, Cambridge 1994, Workshops in Computing, pages 282–294. Springer-Verlag, Berlin, Heidelberg, New York, 1994.
David Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231–274, June 1987.
David Harel, Hagi Lachover, Amnon Naamad, Amir Pnueli, Michal Politi, Rivi Sherman, Aharon Shtull-Trauring, and Mark Trakhtenbrot. Statemate: A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering, 16 No. 4, April 1990.
David Harel and Ammon Naamad. The statemate semantics of statecharts. Technical report, The Weizmann Institute of Science, October 1995.
C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, Eaglewood Cliffs, N.J., 1985.
C. Huizing, R. Gerth, and W. P. de Roever. Modelling statecharts behaviour in a fully abstract way. In Proc. 13th CAAP, volume 299 of Lecture Notes in Computer Science. Springer-Verlag, 1988.
Kolyang, Thomas Santen, and Burkhart Wolff. A structure preserving encoding of Z in Isabelle/HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher-Order Logics, number 1125 in Lecture Notes in Computer Science. Springer-Verlag, Berlin, Heidelberg, New York, 1996.
B. C. Moszkowski. Reasoning about Digital Circuits. PhD thesis, Stanford University, 1983. Tech. Report STAN-CS-83-970.
A. Pnueli and M. Shalev. What is in a step: On the semantics of statecharts. In Takayasu Ito and Albert R. Meyer, editors, Theoretical Aspects of Computer Software, pages 244–264, New York, September 1991. Springer-Verlag. Lecture Notes in Computer Science 526.
J. M. Spivey. The Z Notation. A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992.
Michael von der Beeck. A comparison of statecharts variants.In Langmaak, de Roever, and Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 128–148, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Büssow, R., Grieskamp, W. (1997). Combining Z and temporal interval logics for the formalization of properties and behaviors of embedded systems. In: Shyamasundar, R.K., Ueda, K. (eds) Advances in Computing Science — ASIAN'97. ASIAN 1997. Lecture Notes in Computer Science, vol 1345. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63875-X_42
Download citation
DOI: https://doi.org/10.1007/3-540-63875-X_42
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63875-9
Online ISBN: 978-3-540-69658-2
eBook Packages: Springer Book Archive