This paper gives an overview of a pilot project on the specification and verification of the L4 highperformance microkernel. Of the three aspects examined in the project, we describe one in more detail: the formalisation of the kernel's Application Programming Interface using the B Method. We conclude that machine-supported formal verification of software is at a turning point; that it is now feasible, and desirable, to formally verify production-quality operating systems.
|Cite as: Kolanski, R. and Klein, G. (2006). Formalising the L4 microkernel API. In Proc. Twelfth Computing: The Australasian Theory Symposium (CATS2006), Hobart, Australia. CRPIT, 51. Gudmundsson, J. and Jay, B., Eds. ACS. 53-68. |
(local if available)