Towards applying the composition principle to verify a microkernel operating system.

A compositional proof method allows the components of a system to be specified and verified independently, instead of having to verify the entire system as a monolithic unit. This paper describes how the composition principle of Abadi and Lamport can be applied to specify and compose systems that consist of both safety and progress properties, using the HOL theorem proving system. We discuss the translation of the composition principle into HOL and the resulting proof obligations, and introduce an example system, modeled after a microkernel operating system, that we composed using the method. [ABSTRACT FROM AUTHOR]