Abstract
A simple round-robin real-time scheduler for the MIPS R3000 RISC processor is modelled. Formal verification of its correctness using an interactive theorem prover is then described.
- Title
- Formal specification and interactive proof of a simple real-time scheduler, Technical Report 94-11
- Authors
- Colin Fidge (Author) - University of QueenslandPeter Kearney (Author) - University of QueenslandMark Utting (Author) - University of Queensland
- Publisher
- University of Queensland, Software Verification Research Centre
- Date published
- 1994
- Organisation Unit
- School of Science and Engineering - Legacy; University of the Sunshine Coast, Queensland
- Language
- English
- Record Identifier
- 99449277602621
- Output Type
- Report