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.
Chapter PDF
Similar content being viewed by others
Keywords
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
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.
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.
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.
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.
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.
de Roever, W.P., ‘The Quest for Compositionality', in:E. J. Neuhold and G. Chroust (eds.) Formal Models in Programming, North Holland, 1985.
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.
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.
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.
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.
Williams, Performance pushes RISC chips into real-time roles, Computer Design, September 1991, 79–86.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fidge, C., Kearney, P., Utting, M. (1995). Interactively verifying a simple real-time scheduler. In: Wolper, P. (eds) Computer Aided Verification. CAV 1995. Lecture Notes in Computer Science, vol 939. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60045-0_65
Download citation
DOI: https://doi.org/10.1007/3-540-60045-0_65
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60045-9
Online ISBN: 978-3-540-49413-3
eBook Packages: Springer Book Archive