Combining Z and temporal interval logics for the formalization of properties and behaviors of embedded systems

  • Robert Büssow
  • Wolfgang Grieskamp
Session I
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1345)


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.


Embed System Shared Variable Moderate Extension Dynamic Schema Length Constraint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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.Google Scholar
  2. 2.
    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.Google Scholar
  3. 3.
    Z. Chaochen, C. A. R. Hoare, and A.P Ravn. A calculus of durations. Information Processing Letters, 40(5), 1991.Google Scholar
  4. 4.
    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.Google Scholar
  5. 5.
    David Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231–274, June 1987.CrossRefGoogle Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    David Harel and Ammon Naamad. The statemate semantics of statecharts. Technical report, The Weizmann Institute of Science, October 1995.Google Scholar
  8. 8.
    C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, Eaglewood Cliffs, N.J., 1985.Google Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    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.Google Scholar
  11. 11.
    B. C. Moszkowski. Reasoning about Digital Circuits. PhD thesis, Stanford University, 1983. Tech. Report STAN-CS-83-970.Google Scholar
  12. 12.
    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.Google Scholar
  13. 13.
    J. M. Spivey. The Z Notation. A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992.Google Scholar
  14. 14.
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Robert Büssow
    • 1
  • Wolfgang Grieskamp
    • 1
  1. 1.Institut für Kommunikations- und Softwaretechnik Sekr. FR5-13Technische Universität BerlinBerlinGermany

Personalised recommendations