Formal Verification of the Interrupt Dispatch Program of an Embedded Operating System

The interrupt dispatch program (IDP), a key component of an embedded real-time operating system (RTOS), plays a vital role in context switching and dispatching interrupt service routines (ISRs), which makes it inevitable in the verification of RTOS. We purpose a formal model for verifying the IDP of an automotive embedded RTOS in Isabelle/HOL. We formalize the model by constructing a physical machine state involving both registers and memory and providing relevant operational semantic functions. We also present a methodology for designing the functional logic of the target IDP by subdividing it into different execution scenarios. We establish the implementation correctness theorem in context switching, rescheduling and the relevant mask bit. After carefully reasoning about the behavior of the IDP, we perform the verification of its implementation correctness. Our work provides an important practice for establishing a general method of verification. The idea of formal modeling and verification shown in this paper can be extended to those of other exception handlers and IDPs on different platforms which are considered to be a critical part in the full formal verification of an OS kernel.