Paper Info
Title
Running the manual: an approach to high-assurance microkernel development
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.
Year
DOI
Venue
2006
10.1145/1159842.1159850
Haskell
Keywords
Field
DocType
microkernel development,iterative development,development methodology,formal modelling,precise semi-formal model,iterative refinement,mature final design,machine-checkable formal specification,semi-formal design,development phase,rapid prototyping,higher order logic,operating systems,verification,monads,operating system,formal specification,functional programming language
Specification language,Programming language,Iterative and incremental development,Computer science,Microkernel,Formal specification,Reference implementation,Iterative design,Formal methods,Formal verification
Conference
ISBN
Citations 
PageRank 
1-59593-489-8
22
1.99
References 
Authors
19
5
Name
Order
Citations
PageRank
Philip Derrin172631.12
K. Elphinstone2119065.76
Gerwin Klein3145087.47
David Cock482737.44
Manuel M. T. Chakravarty566641.89