Verifying safety critical task scheduling systems in PPTL axiom system

This paper presents a case study of formal verification of safety critical task scheduling systems. First, a scheduling algorithm described in a temporal logic programming language is presented; then a sufficient and necessary condition for the schedulability of task set is formalized. Further, the correctness of the condition is proved by means of theorem proving in the axiom system of Propositional Projection Temporal Logic.