This paper argues that a pragmatic approach is needed for
integrating design and formalisation of complex systems. We report
on our approach to designing the seL4 operating system
microkernel API and its formalisation in Isabelle/HOL. The
formalisation consists of the systematic translation of significant
parts of the functional programming language Haskell into
Isabelle/HOL, including monad-based code. We give an account of the
experience, decisions and outcomes in this translation as well as
the technical problems we encountered together with our solutions.
The longer-term goal is
to demonstrate that formalisation and verification of a large,
complex, OS-level code base is feasible with current tools and
methods and is in the order of magnitude of traditional development
cost.
@inproceedings{ElphinstoneKK-06,
author = {Kevin Elphinstone and Gerwin Klein and Rafal Kolanski},
title = {Formalising a High-Performance Microkernel},
booktitle = {Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06)},
series = {Microsoft Research Technical Report MSR-TR-2006-117},
year = {2006},
editor = {Rustan Leino},
address = {Seattle, USA},
month = Aug,
pages = {1-7}
}