Verifying a scheduling protocol of safety-critical systems

It is of great importance to ensure safety and reliability of the scheduling protocol of safety-critical systems since the failure will cause serious damage. This paper analyzes a real-time scheduling protocol of a safety-critical system and models it using a Modeling, Simulation and Verification Language program. Further, the schedulability and other desired properties are specified using Propositional Projection Temporal Logic formulas. As a result, these properties are proved with theorem proving and further verified using the runtime verification approach at code level.