Abstract
Duration Calculus, a real-time interval logic, is embedded in Z to provide a specification notation for real time systems that combines the modularisation and abstraction power of Z with reasoning about timing properties in a more convenient logic than first order predicates. The notation is presented through a top level specification of a simple Water Level Monitoring System together with three refinement steps.
This work was initiated while the author was visiting the Technical University of Denmark being sponsored by the ProCoS Project.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Brien S.M, Engel M, Jifeng He, Ravn A.P, Rischel H. Z description of duration calculus. Procos II Report OU HJF 12/2, Oxford University Computing Laboratory, Oxford, England, 1993.
Brien S, Nicholls J, et al. Z base standard. version 1.0. ZIP Report ZIP/PRG/92/121, Oxford University Computing Laboratory, Oxford, England, 1992.
Chaochen Zhou, Hoare C.A.R, Ravn A.P. A calculus of durations. Information Processing Letters, 40 (5): 269–276, 1991.
Chaochen Zhou, Ravn A.P, Hansen M.R. An extended duration calculus for hybrid real-time systems. In Grossman R.L, Nerode A, Ravn A.P, Rischel H (eds), Hybrid Systems. (Lecture Notes in Computer Science, vol. 736), pp 36–59. Berlin: Springer-Verlag, 1993.
Engel M, Kubica M, Madey J, Parnas D.L, Ravn A.P, van Schouwen A.J. A formal approach to computer systems requirements documentation. In Grossman R.L, Nerode A, Ravn A.P, Rischel H (eds), Hybrid Systems. (Lecture Notes in Computer Science, vol. 736), pp 452–474. Berlin: Springer-Verlag, 1993.
Mahony B.P, Hayes I. J. A case-study in timed refinement: A mine pump. IEEE Trans. Softw. Eng., 18 (9): 817–826, 1992.
Parnas D.L, Madey J. Functional documentation for computer systems engineering (version 2). CRL Report 237, Telecommunications Research Institute of Ontario (TRIO), McMaster University, Hamilton, ON, 1991. 14 pp.
Spivey J.M. The Z Notation. A Reference Manual. Prentice-Hall, second edition, 1992.
Schouwen A.J, Parnas D.L, Madey J. Documentation of requirements for computer systems. In Proceeding of the IEEE International Symposium on Requirements Engineering, San Diego, California, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1994 British Computer Society
About this paper
Cite this paper
Engel, M. (1994). Specifying Real-Time Systems with Z and the Duration Calculus. In: Bowen, J.P., Hall, J.A. (eds) Z User Workshop, Cambridge 1994. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3452-7_17
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3452-7_17
Publisher Name: Springer, London
Print ISBN: 978-3-540-19884-0
Online ISBN: 978-1-4471-3452-7
eBook Packages: Springer Book Archive