Formal verification of a task scheduler for embedded operating systems

Abstract

A task scheduler plays an important role in Embedded Operating Systems (EOS). In order to ensure the scheduling properties of an EOS, it is important to verify the implementation of its task scheduler. However, the implementation of a task scheduler requires the manipulation of machine registers directly and uses very complex C pointer structures to manage the task related data. Thus, we need a verification system that can formally describe both C pointer programs and embedded code pointers (e.g., update the stack register) naturally. Based on the Verified Software Toolchain and the CompCert ARM assembly syntax and semantics, we utilize the Coq proof assistant to develop formal reasoning support for the verification of a low-level task scheduler. Our verification system has the capability to verify both C and ARM assembly language; it supports the separation of logical abstractions and specific implementations. More importantly, all the verification can be done in a unified modular verification framework, which minimizes semantic gaps at specification interfaces.