Skip to main content
SpringerLink
Log in

Reasoning about Non-terminating Loops Using Deadline Commands

  • Conference paper
Mathematics of Program Construction (MPC 2000)

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

Included in the following conference series:

Abstract

It is common for a real-time process to consist of a nonterminating loop monitoring an input and controlling an output. Hence a real-time program development method needs to support nonterminating loops. Earlier work on real-time program development has produced a real-time refinement calculus that makes use of a novel deadline command which allows timing constraints to be embedded in real-time programs. The addition of the deadline command to the real-time programming language gives the significant advantage of providing a real-time programming language that is machine independent. This allows a more abstract approach to the program development process.

In this paper we add possibly nonterminating loops to the refinement calculus. First we examine the semantics of possibly nonterminating loops, and use them to reason directly about a simple example. Then we develop simpler refinement rules that make use of a loop invariant.

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. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

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

    Article  Google Scholar 

  3. Floyd, R.W.: Assigning meaning to programs. Math. Aspects of Comput. Sci. 19, 19–32 (1967)

    MathSciNet  Google Scholar 

  4. Grundon, S., Hayes, I.J., Fidge, C.J.: Timing constraint analysis. In: Mc- Donald, C. (ed.) Computer Science 1998: Proc. 21st Australasian Computer Science Conf (ACSC 1998), Perth, February 4–6, pp. 575–586. Springer, Heidelberg (1998)

    Google Scholar 

  5. Hayes, I.J.: Separating timing and calculation in real-time refinement. In: Grundy, J., Schwenke, M., Vickers, T. (eds.) International Refinement Workshop and Formal Methods Pacific 1998, pp. 1–16. Springer, Heidelberg (1998)

    Google Scholar 

  6. 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)

    Google Scholar 

  7. Hayes, I.J., Utting, M.: A sequential real-time refinement calculus. Technical Report UQ-SVRC-97-33, Software Verification Research Centre, The University of Queensland 59 pages (1997), http://svrc.it.uq.edu.au

  8. Hayes, I.J., Utting, M.: Deadlines are termination. In: Gries, D., de Roever, W.-P. (eds.) IFIP TC2/WG2.2, 2.3 International Conference on Programming Concepts and Methods (PROCOMET 1998), pp. 186–204. Chapman and Hall, Boca Raton (1998)

    Google Scholar 

  9. 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)

    Google Scholar 

  10. Hehner, E.C.R.: A Practical Theory of Programming. Springer, Heidelberg (1993)

    MATH  Google Scholar 

  11. Hoare, C.A.R.: An axiomatic approach to computer programming. Comm. ACM 12, 576–580, 583 (1969)

    Article  MATH  Google Scholar 

  12. Hooman, J.: Assertional specification and verification. In: Joseph, M. (ed.) Realtime Systems: Specification, Verification and Analysis, ch. 5, pp. 97–146. Prentice Hall, Englewood Cliffs (1996)

    Google Scholar 

  13. Joseph, M. (ed.): Real-time Systems: Specification, Verification and Analysis. Prentice-Hall, Englewood Cliffs (1996)

    MATH  Google Scholar 

  14. 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., Kim, C.S.: An accurate worst case timing analysis for RISC processors. IEEE Trans. on Software Eng. 21(7), 593–604 (1995)

    Article  Google Scholar 

  15. Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice Hall, Englewood Cliffs (1994)

    MATH  Google Scholar 

  16. Scholefield, D.J.: A Refinement Calculus for Real-Time Systems. PhD thesis, Department of Computer Science, University of York, U.K. (1992)

    Google Scholar 

  17. Scholefield, D.J., Zedan, H., Jifeng, H.: A specification-oriented semantics for the refinement of real-time systems. Theoretical Computer Science 131, 219–241 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  18. Utting, M., Fidge, C.J.: A real-time refinement calculus that changes only time. In: Jifeng, H. (ed.) Proc. 7th BCS/FACS Refinement Workshop. Electronic Workshops in Computing. Springer, Heidelberg (1996), http://www.springer.co.uk/eWiC/Workshops/7RW.html

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Electrical Engineering, The University of Queensland, Brisbane, 4072, Australia

    Ian Hayes

Authors
  1. Ian Hayes
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science, University of Nottingham, NG8 1BB, Nottingham, England

    Roland Backhouse

  2. Dep. Informática, Universidade do Minho, Campus de Gualtar, P.O. Box, 4700-320, Braga, Portugal

    José Nuno Oliveira

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hayes, I. (2000). Reasoning about Non-terminating Loops Using Deadline Commands. In: Backhouse, R., Oliveira, J.N. (eds) Mathematics of Program Construction. MPC 2000. Lecture Notes in Computer Science, vol 1837. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722010_5

Download citation

  • DOI: https://doi.org/10.1007/10722010_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67727-7

  • Online ISBN: 978-3-540-45025-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation