Skip to main content
SpringerLink
Log in

Towards a Refinement Calculus for Concurrent Real-Time Programs

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2002)

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

Included in the following conference series:

Abstract

We define a language and a predicative semantics to model concurrent real-time programs. We consider different communication paradigms between the concurrent components of a program: communication via shared variables and asynchronous message passing (for different models of channels).

The semantics is the basis for a refinement calculus to derive machine-independent concurrent real-time programs from specifications. We give some examples of refinement laws that deal with concurrency.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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 and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer, 1998.

    Google Scholar 

  2. R. J. R. Back. A calculus of refinement for program derivations. Acta Informatica, 25:593–624, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  3. E. W. Dijkstra. A Discipline of Programming. Prentice-Hall Series in Automatic Computation. Prentice Hall, 1976.

    Google Scholar 

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

    Article  Google Scholar 

  5. S. Grundon, I. Hayes, and C. Fidge. Timing constraint analysis. In C. McDonald, editor, Computer Science’ 98: Proc. 21st Australasian Computer Science Conference, pages 575–586. Springer-Verlag, Singapore, 1998.

    Google Scholar 

  6. I. Hayes. Real-time program refinement using auxiliary variables. In M. Joseph, editor, Proc.6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems,volume 1926 of LNCS, pages 170–184. Springer, 2000.

    Chapter  Google Scholar 

  7. I. J. Hayes, C. J. Fidge, and K. Lermer. Semantic characterisation of dead control-flow paths. IEE Proceedings-Software, 148(6): 175–186, December 2001.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  9. E. C. R. Hehner. A Practical Theory of Programming. Springer, 1993.

    Google Scholar 

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

    Article  Google Scholar 

  11. C. Morgan. Programming from Specifications, 2nd edition. International Series in Computer Science. Prentice Hall, 1994.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  13. N. Wirth. Program development by stepwise refinement. Communications of the ACM, 14(4):221–227, 1971.

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Verification Research Centre, The University of Queensland, Australia

    Sibylle Peuker

  2. School of Information Technology and Electrical Engineering, The University of Queensland, Australia

    Ian Hayes

Authors
  1. Sibylle Peuker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ian Hayes
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. International Institute for Software Technology, United Nations University, Casa Silva Mendes, Est. do Engenheiro Trigo No. 4, P.O. Box 3058, Macao

    Chris George

  2. School of Computer Engineering and Science, Shanghai University, 149 Yanchang Road, Shanghai, 200072, P.R. China

    Huaikou Miao

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Peuker, S., Hayes, I. (2002). Towards a Refinement Calculus for Concurrent Real-Time Programs. In: George, C., Miao, H. (eds) Formal Methods and Software Engineering. ICFEM 2002. Lecture Notes in Computer Science, vol 2495. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36103-0_35

Download citation

  • DOI: https://doi.org/10.1007/3-540-36103-0_35

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-36103-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation