In ACM
SIGPLAN 2006 Haskell Workshop, ACM Press, 2006.
Abstract
We propose a development methodology for designing and prototyping
high assurance microkernels, and describe our application of it. The
methodology is based on rapid prototyping and iterative refinement
of the microkernel in a functional programming language. The
prototype provides a precise semi-formal model, which is also
combined with a machine simulator to form a reference implementation
capable of executing real user-level software, to obtain accurate
feedback on the suitability of the kernel API during development
phases. We extract from the prototype a machine-checkable
formal specification in higher-order logic, which may be used to
verify properties of the design, and also results in corrections to
the design without the need for full verification. We found the approach
leads to productive, highly iterative development where formal
modelling, semi-formal design and prototyping, and end use all
contribute to a more mature final design in a shorter period of
time.
PDF preprint (12 pages)
This page is part of Manuel Chakravarty's WWW-stuff.