Component-based approach to run-time kernel specification and verification

The traditional approach to high-integrity embedded system development has been to develop and verify the application with the assumption that either the operating system services have deterministic behaviour with well understood operational semantics or that the operating system itself is certified. Formal verification approaches have focused on modelling the application at the right level of abstraction and verifying specific properties based on the model. The effective use of formal methods in high-integrity embedded system development requires efficient models of both the application and the underlying operating system services. Software implemented operating systems pose significant complexity constraints in terms of creating usable models. This paper presents a component-based formal model of a hardware-implemented run-time kernel. It builds on work carried out earlier for the LAMR kernel (K. Lundqvist and L. Asplund, 2003). The components are designed to allow easy deployment, and can be replicated to enable system growth. Additionally, the kernel presented in this paper supports multiprocessor scheduling.