Abstract
We have recently extended the sequential refinement calculus to handle real-time programs. A novel deadline command allows execution time limits to be expressed in a high-level language. The calculus allows refinement steps that separate timing constraints from non-timing requirements. Rules are provided for handling timing constraints, but the refinement of components implementing non-timing requirements is essentially the same as in the standard refinement calculus.
In this paper, we present a new refinement rule for loops that does not require a variant for termination, but uses a deadline command instead. To illustrate the calculus and the new loop introduction rule, we present an example refinement of a program that calculates the size of a kiwifruit from the time it takes to pass through a light beam.
Chapter PDF
Similar content being viewed by others
References
Back, R.-J. (1980) Corrcctness preserving program refinements: Proof theory and applications. Tract 131, Mathematisch Centrum, Amsterdam.
Grundon, S., Hayes, I. J. and Fidge, C. J. (1988) Timing constraint analysis, in C. Mcdonald, ed., Computer Science 98: Proc. 21st Austraalasian Computer Science Conf. (ACSC’98) Perth. 4–6 Feb.’ Springer-Verlag, pp. 575–586.
Hayes. I. J. and Mahony, B. P. (1995) ‘Using units of measurement in formal specifications’. Formal Aspects of Computing 7 (3), 329–347.
Hayes, I. and Utting. M. (1997a) Coercing real-time refinement: A transmitter, in D. J. Duke and A. S. Evans, eds, ‘BCS-FACS Northern Formal Methods Workshop’, Electronic Workshops in Computing, Springer Verlag. URL http://www.springer.co.uk/ewic/workshops/NFM96/.
Hayes, I. and Utting, M. (1997b) A sequential real-time refinement calculus. Technical Report UQ-SVRC-97–33, Software Verification Research Centre, The University of Queensland, URL http://svrc. It.uq.edu.au.
Lim, S.-S., Bae, Y. H., Jang, G. T., Rhee, B.-D., Min, S. L., Park, C. Y., Shin, H., Park, K., Moon, S.-M. and Kim, C. S. (1995) ‘An accurate worst case timing analysis for RISC processors’, IEEE Trans. On Software Eng. 21(7)593–604.
Mahony, B. P. (1992) The Specification and Refinement of Timed Processes. Phd thesis, Department of Computer Science, The University of Queensland.
Morgan, C. (1994) Programming from Specifications. Second edn, Prentice Hall.
Utting, M. and Fidge, C. (1996) A real-time refinement calculus that changes only time, in He Jifeng, ed. ‘Proc. 7th BCS/FACS Refinement Workshop’, Electronic Workshops in Computing, Springer. .
Utting, M. and Fidge, C. J. (1997) Refinement of infeasible real-time programs, in Proc. Formal Mehtods Pacific ‘97’, Discrete Mathematics and Theoretical Computer Science, Springer, Wellington, New Zealand, pp. 243–262.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Hayes, I.J., Utting, M. (1998). Deadlines are termination. In: Gries, D., de Roever, WP. (eds) Programming Concepts and Methods PROCOMET ’98. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35358-6_15
Download citation
DOI: https://doi.org/10.1007/978-0-387-35358-6_15
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6299-0
Online ISBN: 978-0-387-35358-6
eBook Packages: Springer Book Archive