Abstract
Real-time program development can be split into a machine- independent phase, that deriv es a machine-independent real-time program from a specification, and a machine-dependent phase, that checks that the compiled program will meet its deadlines when executed on the target machine.
In this paper we extend a machine-independent real-time programming language with auxiliary variables. These are introduced to facilitate both reasoning about the correctness of real-time programs and the expression of timing deadlines, and hence the calculation of timing constraints on paths through a program. The auxiliary variable concept is extended to auxiliary parameters to procedures.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
C. J. Fidge, I. J. Hayes, and G. Watson. The deadline command. IEE Proceedings Software, 146(2):104–111, April 1999.
S. Grundon, I. J. Hayes, and C. J. Fidge. Timing constraint analysis. In C. Mc-Donald, editor, Computer Science’ 98: Proc. 21st Australasian Computer Science Conf. (ACSC’98), Perth, 4-6 Feb., pages 575–586. Springer-Verlag, 1998.
I. J. Hayes. Reasoning about non-terminating loops using deadline commands. In Roland Backhouse and Jose Oliveira, editors, Mathematics of Program Construction (MPC’2000), July 2000.
I. J. Hayes, C. J. Fidge, and K. Lermer. Semantic identification of dead control-flow paths. Technical Report 99-32, Software Verification Research Centre, The University of Queensland, October 1999.
I. J. Hayes and B. P. Mahony. Using units of measurement in formal specifications. Formal Aspects of Computing, 7(3):329–347, 1995.
I. J. Hayes and M. Utting. Coercing real-time refinement: A transmitter. In D. J. Duke and A. S. Evans, editors, BCS-FACS Northern Formal Methods Workshop (NFMW’96), Electronic Workshops in Computing. Springer Verlag, 1997.
I. J. Hayes and M. Utting. 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, 1997.
E. C. R. Hehner. Termination is timing. In J.L.A. van de Snepscheut, editor, Mathematics of Program Construction, volume 375 of Lecture Notes in Computer Science, pages 36–47. Springer-Verlag, June 1989.
E. C. R. Hehner. A Practical Theory of Programming. Springer Verlag, 1993.
J. Hooman and O. van Roosmalen. Formal design of real-time systems in a platform-independent way. Parallel and Distributed Computing Practices, 1(2):15–30, 1998.
Sung-Soo Lim, Young Hyun Bae, Gyu Tae Jang, Byung-Do Rhee, Sang Lyul Min, Chang Yun Park, Heonshik Shin, Kunsoo Park, Soo-Mook Moon, and Chong Sang Kim. An accurate worst case timing analysis for RISC processors. IEEE Trans. on Software Eng., 21(7):593–604, July 1995.
C. C. Morgan. Programming from Specifications. Prentice Hall, second edition,1994.
M. Utting and C. J. Fidge. A real-time refinement calculus that changes only time. In He Jifeng, editor, Proc. 7th BCS/FACS Refinement Workshop, Electronic Workshops in Computing. Springer, July 1996. URL http://www.springer.co.uk/eWiC/Workshops/7RW.html.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hayes, I. (2000). Real-Time Program Refinement Using Auxiliary Variables. In: Joseph, M. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 2000. Lecture Notes in Computer Science, vol 1926. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45352-0_15
Download citation
DOI: https://doi.org/10.1007/3-540-45352-0_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41055-3
Online ISBN: 978-3-540-45352-9
eBook Packages: Springer Book Archive