Advertisement

Interactively verifying a simple real-time scheduler

  • Colin Fidge
  • Peter Kearney
  • Mark Utting
Session 11: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

Abstract

This paper describes the interactive verification of a simple interrupt-driven real-time scheduler written in the machine code language of the MIPS R3000 RISC processor. The formal verification was carried out using the interactive theorem prover Ergo.

Keywords

Instruction Cache Task Behaviour Machine Cycle Interrupt Handler Interactive Theorem Prover 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Fidge, C., Kearney, P., and Utting, M., ‘Formal Specification and Interactive Proof of a Simple Real-time Scheduler', Technical Report 94-11, Software Verification Research Centre, Department of Computer Science. April 1994.Google Scholar
  2. 2.
    Griffiths, A., and Utting, M., ‘The Automatic Proof of Theorems Involving Linear Inequalities', Technical Report 94-29, Software Verification Research Centre, Department of Computer Science.Google Scholar
  3. 3.
    Kearney, P., Staples, J., Abbas, A., ‘Functional Verification of Hard Real-Time Programs', in Algorithms, Software, Architecture, ed. L. van Lueewen, Information Processing 92, Volume I, North-Holland 1992, 113–119.Google Scholar
  4. 4.
    Kearney, P., Staples, J., Abbas, A. and Liu, C., ‘Functional Verification of Real-Time Procedural Code: a Simplified RS232 Software Repeater Problem', Technical Report 91-2, Software Verification Research Centre, Department of Computer Science. Revised, May 1992.Google Scholar
  5. 5.
    Kearney, P., and Utting., M., ‘A Layered Real-time Specification of a RISC Processor', in: Langmaack, H., de Roever, W.-P. and Vytopil J., eds., Formal Techniques in Real-time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863, September 1994, pp. 455–475.Google Scholar
  6. 6.
    de Roever, W.P., ‘The Quest for Compositionality', in:E. J. Neuhold and G. Chroust (eds.) Formal Models in Programming, North Holland, 1985.Google Scholar
  7. 7.
    Staples J., Robinson, P., Hazel, D., ‘A functional logic for higher level reasoning about computation', Formal Aspects of Computing, Vol. 6, pages 1–38, 1994.Google Scholar
  8. 8.
    Utting, M., ‘Instruction-level Specification of a MIPS R3000 CPU', Software Verification Research Centre Technical Report 93-26, February 1994, revised April 1994, 27 pages.Google Scholar
  9. 9.
    Utting, M., Kearney, P., ‘Pipeline Specification of a MIPS R3000 CPU', Software Verification Research Centre Technical Report 92-6, October 1992, revised April 1994, 57 pages.Google Scholar
  10. 10.
    Utting, M. and Whitwell, K., ‘Ergo 4.0 Users Manual', Technical Report 93–19, Software Verification Research Centre, Department of Computer Science, University of Queensland, 1994.Google Scholar
  11. 11.
    Williams, Performance pushes RISC chips into real-time roles, Computer Design, September 1991, 79–86.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Colin Fidge
    • 1
  • Peter Kearney
    • 1
  • Mark Utting
    • 1
  1. 1.Software Verification Research Centre, Department of Computer ScienceThe University of QueenslandBrisbaneAustralia

Personalised recommendations