IFM’99 pp 49-65 | Cite as

Towards Real-Time Object-Z

  • Graeme Smith
  • Ian Hayes


This paper presents a method of formally specifying systems involving continuous variables and real-time constraints using the object-oriented state-based specification language Object-Z together with the timed trace notation of the timed refinement calculus. The basis of this integration is a mapping of the existing Object-Z history semantics to timed traces.


Finish Time Proof Obligation Digital Thermometer Local Constant Cache Coherence Protocol 
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]
    J.S. Dong, J. Colton, and L. Zucconi. A formal object approach to realtime specification. In 3rd Asia-Pacific Software Engineering Conference (APSEC’96). IEEE Computer Society Press, 1996.Google Scholar
  2. [2]
    J.S. Dong, R. Duke, and G. Rose. An object-oriented approach to the semantics of programming languages. In G. Gupta, editor, 17th Annual Computer Science Conference (ACSC’17), pages 767–775, 1994.Google Scholar
  3. [3]
    K. Duddy, L. Everett, C. Millerchip, B.P. Mahony, and I.J. Hayes. Z-based notation for the specification of timing properties. Department of Computer Science, University of Queensland, June 1995.Google Scholar
  4. [4]
    R. Duke, G. Rose, and G. Smith. Object-Z: A specification language advocated for the description of standards. Computer Standards and Interfaces, 17:511–533, 1995.CrossRefGoogle Scholar
  5. [5]
    C.J. Fidge, I.J. Hayes, and B.P. Mahony. Defining differentiation and integration in Z. In J. Staples, M.G. Hinchey, and Shaoying Liu, editors, IEEE International Conference on Formal Engineering Methods (ICFEM ’98), pages 64–73. IEEE Computer Society, 1998.Google Scholar
  6. [6]
    C.J. Fidge, I.J. Hayes, A.P. Martin, and A.K. Wabenhorst. A set-theoretic model for real-time specification and reasoning. In J. Jeuring, editor, Mathematics of Program Construction (MPC’98), volume 1422 of LNCS, pages 188–206. Springer-Verlag, 1998.CrossRefGoogle Scholar
  7. [7]
    C. Fischer. CSP-OZ - a combination of CSP and Object-Z. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems. Chapman & Hall, 1997.Google Scholar
  8. [8]
    V. Friesen. An exercise in hybrid system specification using an extension of Z. In A. Bouajjani and O. Maler, editors, Proceedings Second European Workshop on Real-Time and Hybrid Systems, pages 311–316. VERIMAG Laboratory, Grenoble, 1995.Google Scholar
  9. [9]
    R. Geisler, M. Klar, and C. Pons. Dimensions and dichotomy in metamod-eling. In D.J. Duke and A.S. Evans, editors, Proceedings 3rd BCS-FACS Northern Formal Methods Workshop, 1998.Google Scholar
  10. [10]
    ISO/IEC JTC1/SC24 N1152. Report of the ISO/IEC JTC/SC24 Special Rapporteur Group on Formal Description Techniques, May 1994.Google Scholar
  11. [11]
    W. Johnston. A type checker for Object-Z. Technical Report 96–24, Software Verification Research Centre, University of Queensland, 1996.Google Scholar
  12. [12]
    B.P. Mahony. The Specification and Refinement of Timed Processes. PhD thesis, Department of Computer Science, University of Queensland, 1992.Google Scholar
  13. [13]
    B.P. Mahony. Using the refinement calculus for dataflow processes. Technical Report 94–32, Software Verification Research Centre, University of Queensland, October 1994.Google Scholar
  14. [14]
    B.P. Mahony and J.S. Dong. Blending Object-Z and Timed CSP: An introduction to TCOZ. In 20th International Conference on Software Engineering. IEEE Press, 1998.Google Scholar
  15. [15]
    B.P. Mahony and J.S. Dong. Sensors and actuators: Process control in TCOZ. Technical Report 98–38, Mathematical and Information Sciences, Commonwealth Scientific and Industrial Research Organisation (CSIRO), Australia, 1998.Google Scholar
  16. [16]
    B.P. Mahony and I.J. Hayes. A case-study in timed refinement: A mine pump. IEEE Transactions on Software Engineering, 18(9):817—826, September 1992.CrossRefGoogle Scholar
  17. [17]
    W.R. Oliveira and R.S.M. Barros. The real numbers in Z. In D.J. Duke and A.S. Evans, editors, 2nd BCS-FACS Northern Formal Methods Workshop, Electronic Workshops in Computing. Springer-Verlag, 1998.Google Scholar
  18. [18]
    K. Periyasamy and V.S. Alagar. Extending Object-Z for specifying realtime systems. In TOOLS USA ’97: Technology of Object-Oriented Languages and Systems, pages 163–175. IEEE Computer Society Press, 1998.Google Scholar
  19. [19]
    G. Rose and R. Duke. An Object-Z specification of a mobile phone system. In K. Lano and H. Haughton, editors, Object-Oriented Specification Case Studies, Object-Oriented Series. Prentice Hall, 1993.Google Scholar
  20. [20]
    G. Smith. A fully abstract semantics of classes for Object-Z. Formal Aspects of Computing, 7(3):289–313, 1995.CrossRefGoogle Scholar
  21. [21]
    G. Smith. A semantic integration of Object-Z and CSP for the specification of concurrent systems. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, Formal Methods Europe (FME’97), volume 1313 of LNCS, pages 62–81. Springer-Verlag, 1997.Google Scholar
  22. [22]
    G. Smith and R. Duke. Modelling a cache coherence protocol using Object- Z. In 13th Australian Computer Science Conference (ACSC-13), pages 352–361, 1990.Google Scholar
  23. [23]
    J.M. Spivey. The Z Notation: A Reference Manual Prentice Hall, 2nd edition, 1992.Google Scholar
  24. [24]
    Zhou Chaochen, C.A.R. Hoare and A.P. Ravn. A calculus of durations. Information Processing Letters, 40:269–271, December 1991.MathSciNetMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag London Limited 1999

Authors and Affiliations

  • Graeme Smith
    • 1
  • Ian Hayes
    • 1
    • 2
  1. 1.Software Verification Research CentreAustralia
  2. 2.Department of Computer Science and Electrical EngineeringUniversity of QueenslandAustralia

Personalised recommendations