Formalising the L4 microkernel API

Kolanski, R. and Klein, G.

    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.
pdf (from crpit.com) pdf (local if available) BibTeX EndNote GS