Skip to main content
SpringerLink
Log in

The Real-Time Refinement Calculus: A Foundation for Machine-Independent Real-Time Programming

  • Conference paper
  • First Online:
Book cover Application and Theory of Petri Nets 2002 (ICATPN 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2360))

Included in the following conference series:

Abstract

The real-time refinement calculus is an extension of the standard refinement calculus in which programs are developed from a precondition plus post-condition style of specification. In addition to adapting standard refinement rules to be valid in the real-time context, specific rules are required for the timing constructs such as delays and deadlines. Because many real-time programs may be nonterminating, a further extension is to allow nonterminating repetitions.

A real-time specification constrains not only what values should be output, but when they should be output. Hence for a program to implement such a specification, it must guarantee to output values by the specified times. With standard programming languages such guarantees cannot be made without taking into account the timing characteristics of the implementation of the program on a particular machine. To avoid having to consider such details during the refinement process, we have extended our real-time programming language with a deadline command. The deadline command takes no time to execute and always guarantees to meet the specified time; if the deadline has already passed the deadline command is infeasible (miraculous in Dijkstra’s terminology).When such a real-time program is compiled for a particular machine, one needs to ensure that all execution paths leading to a deadline are guaranteed to reach it by the specified time. We consider this checking as part of an extended compilation phase. The addition of the deadline command restores for the real-time language the advantage of machine independence enjoyed by non-real-time programming languages.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R.-J. Back. Correctness preserving program refinements: Proof theory and applications. Tract 131, Mathematisch Centrum, Amsterdam, 1980.

    MATH  Google Scholar 

  2. E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

    Google Scholar 

  3. C. J. Fidge, I. J. Hayes, and G. Watson. The deadline command. IEE Proceedings— Software, 146(2):104–111, April 1999.

    Google Scholar 

  4. S. Grundon, I. J. Hayes, and C. J. Fidge. Timing constraint analysis. In C. McDonald, editor, Computer Science’ 98: Proc. 21st Australasian Computer Sci. Conf. (ACSC’98), Perth, 4–6 Feb., pages 575–586. Springer, 1998.

    Google Scholar 

  5. I. J. Hayes. Real-time program refinement using auxiliary variables. In M. Joseph, editor, Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1926 of Lecture Notes in Comp. Sci., pages 170–184. Springer, 2000.

    Chapter  Google Scholar 

  6. I. J. Hayes. Reasoning about non-terminating loops using deadline commands. In R. Backhouse and J. N. Oliveira, editors, Proc. Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pages 60–79. Springer, 2000.

    Chapter  Google Scholar 

  7. I. J. Hayes. A predicative semantics for real-time refinement. In A. McIver and C. C. Morgan, editors, Essays in Programming Methodology. Springer, 2002. 26 pages. Accepted.

    Google Scholar 

  8. I. J. Hayes. Reasoning about real-time repetitions: Terminating and nonterminating. Science of Computer Programming, 2002. 32 pages. Accepted.

    Google Scholar 

  9. I. J. Hayes and B. P. Mahony. Using units of measurement in formal specifications. Formal Aspects of Computing, 7(3):329–347, 1995.

    Article  Google Scholar 

  10. 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). Springer, 1997.

    Google Scholar 

  11. I. J. Hayes and M. Utting. A sequential real-time refinement calculus. Acta Informatica, 37(6):385–448, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  12. J. Hooman and O. van Roosmalen. An approach to platform independent real-time programming: (1) formal description. Real-Time Systems, 19(1):61–85, July 2000.

    Google Scholar 

  13. C. B. Jones. Program specification and verification in VDM. Technical Report UMCS-86-10-5, Department of Computer Science, University of Manchester, 1986.

    Google Scholar 

  14. C.C. Morgan. The specification statement. ACM Trans. Prog. Lang. and Sys., 10(3), July 1988.

    Google Scholar 

  15. N. Wirth. Program development by stepwise refinement. Comm. ACM, 14(4):221–227, 1971.

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Information Technology and Electrical Engineering, The University of Queensland, Brisbane, 4072, Australia

    Ian J. Hayes

Authors
  1. Ian J. Hayes
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Division of Informatics, University of Edinburgh, James Clerk Maxwell Building, The King’s Buildings Mayfield Road, Edinburgh, EH9 3JZ, UK

    Javier Esparza

  2. Department of Computer Science, University of Adelaide, North Terrace, Adelaide, SA, 5005, Australia

    Charles Lakos

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hayes, I.J. (2002). The Real-Time Refinement Calculus: A Foundation for Machine-Independent Real-Time Programming. In: Esparza, J., Lakos, C. (eds) Application and Theory of Petri Nets 2002. ICATPN 2002. Lecture Notes in Computer Science, vol 2360. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48068-4_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-48068-4_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43787-1

  • Online ISBN: 978-3-540-48068-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation