Termination of real-time programs: Definitely, definitely not, or maybe

Hayes, I. J. (2006). Termination of real-time programs: Definitely, definitely not, or maybe. In: S. Dunne and B. Stoddart, Unifying Theories of Programming. First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, (141-154). 5 - 7 February, 2006. doi:10.1007/11768173_9

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Hayes, I. J.
Title of paper Termination of real-time programs: Definitely, definitely not, or maybe
Conference name First International Symposium, UTP 2006
Conference location Walworth Castle, County Durham, UK
Conference dates 5 - 7 February, 2006
Proceedings title Unifying Theories of Programming   Check publisher's open access policy
Journal name Lecture Notes in Computer Science   Check publisher's open access policy
Place of Publication Heidelberg
Publisher Springer Verlag
Publication Year 2006
Sub-type Fully published paper
DOI 10.1007/11768173_9
Open Access Status DOI
ISBN 978-3-540-34750-7/0302-9743
ISSN 0302-9743
Editor S. Dunne
B. Stoddart
Volume 4010
Start page 141
End page 154
Total pages 14
Language eng
Abstract/Summary 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.
Subjects E1
280302 Software Engineering
700199 Computer software and services not elsewhere classified
Keyword Computer Science, Theory & Methods
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status UQ

Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 5 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 7 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Fri, 24 Aug 2007, 07:40:17 EST