System-Level Verification of Embedded Operating Systems Components

The increasing complexity of embedded operating systems is pushing their design to System-Level, leading to the convergence between software and hardware. In such scenario, it is highly desirable to verify system properties formally, regardless of whether their components are going to be implemented in software or hardware. In this paper, we introduce an approach to verify functional correctness and safety properties of embedded operating system components formally and at System-Level. In order to demonstrate our approach, we present a scheduler of an embedded operating system showing that such scheduler follows its specification regardless of the domain it is instantiated. The verified code was subsequently compiled using GCC yielding a software instance and using CatapultC yielding a hardware instance of the scheduler.