Skip to main content
SpringerLink
Log in

A mechanized theory for the verification of real-time program code using higher order logic

  • Session 7B
  • Conference paper
  • First Online:
Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 1992)

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

  • 176 Accesses

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 1940.

    Google Scholar 

  2. A. Camilleri, P. Iverardi, and M. Nesi. Combining interaction and automation in process algebra verification. In TAPSOFT '91, number 494 in Lecture Notes in Computer Science, pages 283–296. Springer Verlag, April 1991.

    Google Scholar 

  3. Rachel Cardell-Oliver. Using higher order logic for modelling real-time protocols. In TAPSOFT '91, number 494 in Lecture Notes in Computer Science, pages 259–282. Springer Verlag, April 1991.

    Google Scholar 

  4. M.J.C. Gordon, A.J.R.G. Milner, and C.P. Wadsworth. Edinburgh LCF: a mechanized logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer Verlag, 1979.

    Google Scholar 

  5. Michael J.C. Gordon. Mechanizing programming logics in higher order logic. Technical Report 145, Computer Laboratory, University of Cambridge, September 1988. published in 1988 Banff Conf on Hardware Verification.

    Google Scholar 

  6. Mike Gordon. Hard real time. In Fourth Refinement Workshop, pages 00–00. BCS FACS and Logica Cambridge, January 1991.

    Google Scholar 

  7. Volkmar H. Haase. Real-time behaviour of programs. IEEE Transactions on Software Engineering, pages 494–501, September 1981.

    Google Scholar 

  8. Roger Hale. Safe/0. Draft Document, May 1990.

    Google Scholar 

  9. Eric C R Hehner. Real-time programming. Information Processing Letters, 30:51–56, 16 January 1989.

    Google Scholar 

  10. Jozef Hooman. A compositional proof theory for real-time distributed message passing. In PARLE: Parallel Architectures and Languages Europe. Volume II, pages 315–332, June 1987. Springer Verlag Lecture Notes in Computer Science 259.

    Google Scholar 

  11. Ministry of Defence. Interim Defence Standard 00–55. The Procurement of Safety Critical Software in Defence Equipment. 5 April 1991

    Google Scholar 

  12. Johnathan S. Ostroff. Temporal Logic for Real-Time Systems. Research Studies Press, 1989.

    Google Scholar 

  13. Alan C. Shaw. Reasoning about time in higher-level language software. IEEE Transactions on Software Engineering, 15(7):875–889, Jul 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Laboratory, University of Cambridge DSTO, Australia

    Rachel Cardell-Oliver

Authors
  1. Rachel Cardell-Oliver
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jan Vytopil

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cardell-Oliver, R. (1991). A mechanized theory for the verification of real-time program code using higher order logic. In: Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1992. Lecture Notes in Computer Science, vol 571. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55092-5_21

Download citation

  • DOI: https://doi.org/10.1007/3-540-55092-5_21

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-46692-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation