Ingredients of Operating System Correctness:
Lessons Learned in the Formal Verification of PikeOS
Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer
In the context of the Verisoft XT project functional correctness of the
microkernel of PikeOS from SYSGO AG is shown at the source code level using
the VCC verification tool, developed by Microsoft Research. In this paper we
outline a simulation theorem between a top-level abstract model and the system
consisting of the kernel and user programs running in alternation on the real
machine. Based on an example of a typical code trace through the kernel, we
identify the correctness properties of all components in the trace that are
needed for the overall correctness proof of the microkernel.