Formal Modelling of Separation Kernel Components

Abstract. Separation kernels are key components in embedded applications. Their small size and widespread use in high-integrity environments make them good targets for formal modelling and verification. We summarise results from the mechanisation of a separation kernel scheduler using the Z/Eves theorem prover. We concentrate on key data structures to model scheduler operations. The results are part of an experiment in a Grand Challenge in software verification, as part of a pilot project in verified OS kernels. The project aims at creating a mechanised formal model of kernel components that gets refined to code. This provides a set of reusable components, proof strategies, and general lemmas. Important findings about properties and requirements are also discussed.

• Type: Journal
• Year: 2010
• Where: ICTAC
• Authors: Andrius Velykis, Leo Freitas
• Keywords: Applied Computing, ICTAC 2010, Key Data Structures, Separation Kernel, Separation Kernel Scheduler