Abstract
Real-time control programs are often used in contexts where (conceptually) they run forever. Repetitions within such programs (or their specifications) may either (i) be guaranteed to terminate, (ii) be guaranteed to never terminate (loop forever), or (iii) may possibly terminate. In dealing with real-time programs and their specifications, we need to be able to represent these possibilities, and define suitable refinement orderings.
A refinement ordering based on Dijkstra’s weakest precondition only copes with the first alternative. Weakest liberal preconditions allow one to constrain behaviour provided the program terminates, which copes with the third alternative to some extent. However, neither of these handles the case when a program does not terminate. To handle this case a refinement ordering based on relational semantics can be used. In this paper we explore these issues and the definition of loops for real-time programs as well as corresponding refinement laws.
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
Cohen, E.: Hypotheses in Kleene algebra. Technical report TM-ARH-023814, Bellcore (1994)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Dunne, S.E.: Recasting Hoare and He’s unifying theory of programs in the context of general correctness. In: Butterfield, A., Strong, G., Pahl, C. (eds.) Proceedings of the 5th Irish Workshop in Formal Methods, IWFM 2001, Workshops in Computing. British Computer Society (2001), http://ewic.bcs.org/conferences/2001/5thformal/papers
Fidge, C.J., Hayes, I.J., Watson, G.: The deadline command. IEE Proceedings—Software 146(2), 104–111 (1999)
Hayes, I.J.: Real-time program refinement using auxiliary variables. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 170–184. Springer, Heidelberg (2000)
Hayes, I.J.: Reasoning about real-time repetitions: Terminating and nonterminating. Science of Computer Programming 43(2–3), 161–192 (2002)
Hayes, I.J.: A predicative semantics for real-time refinement. In: McIver, A., Morgan, C.C. (eds.) Programming Methodology, pp. 109–133. Springer, Heidelberg (2003)
Hayes, I.J., Utting, M.: Coercing real-time refinement: A transmitter. In: Duke, D.J., Evans, A.S. (eds.) BCS-FACS Northern Formal Methods Workshop (NFMW 1996). Electronic Workshops in Computing. Springer, Heidelberg (1997)
Hayes, I.J., Utting, M.: A sequential real-time refinement calculus. Acta Informatica 37(6), 385–448 (2001)
Hayes, I.J.: Programs as paths: An approach to timing constraint analysis. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 1–15. Springer, Heidelberg (2003)
Hehner, E.C.R.: Termination is timing. In: van de Snepscheut, J.L.A. (ed.) MPC 1989. LNCS, vol. 375, pp. 36–47. Springer, Heidelberg (1989)
Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)
Jones, C.B.: Program specification and verification in VDM. Technical Report UMCS-86-10-5, Department of Computer Science, University of Manchester (1986)
Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems 19(3), 427–443 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hayes, I.J. (2006). Termination of Real-Time Programs: Definitely, Definitely Not, or Maybe. In: Dunne, S., Stoddart, B. (eds) Unifying Theories of Programming. UTP 2006. Lecture Notes in Computer Science, vol 4010. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11768173_9
Download citation
DOI: https://doi.org/10.1007/11768173_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34750-7
Online ISBN: 978-3-540-34752-1
eBook Packages: Computer ScienceComputer Science (R0)