This paper gives an overview of a pilot project on the specification and
verification of the L4 high-performance 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.
@inproceedings{KolanskiK-06,
author = {Rafal Kolanski and Gerwin Klein},
title = {Formalising the {L4} microkernel {API}},
booktitle = {Computing: The Australasian Theory Symposium (CATS 06)},
year = {2006},
editor = {Barry Jay and Joachim Gudmundsson},
address = {Hobart, Australia},
month = Jan,
pages = {53--68},
series = {Conferences in Research and Practice in Information Technology},
volume = {51}
}