Formal Verification of Distributed Preemptive Real-time Scheduling

The application of component middleware in missioncritical systems introduces new challenges for distributed real-time embedded (DRE) system developers such as the safe composition of components to ensure end-to-end predictability. Model-based analysis provides a way to evaluate design alternatives with respect to functional specifications and the target platform. This paper introduces a semantic domain which captures key time-based properties of a generic class of DRE systems. We utilize this semantic domain to verify the preemptive schedulability using existing model checking tools. The proposed verification method and framework is demonstrated on a mission-critical avionics DRE system. 1