Formal Modeling and Verification of the Sequential Kernel of an Embedded Operating System

A formal computational model is presented for the sequential kernel of an automotive embedded real-time operating system, which provides infrastructural mechanism to support the isolation between applications and the operating system, as well as the isolation between executive entities such as tasks and ISRs (Interrupt Service Routines) in applications. The target embedded system is modeled at the granularity of isolated memory regions and stacks. Tasks, nested ISRs and the preempt-able part of the operating system (i.e. system services) are concurrent entities executing on dedicated memory regions and stacks determined by the sequential kernel. States of these entities can be correctly saved and restored in isolated stacks and in the kernel data structures, such that the control flow changes among them can be correctly made. The implementation correctness theorem of the kernel is established along with the corresponding simulation relationship and implementation invariants. According to the features of the model and the related implementation languages, the kernel is formally verified with the theorem prover Isabelle/HOL.