Formal analysis for real-time scheduling

A sound theory of real-time scheduling is necessary to support the engineering of real-time software applications. Developing scheduling results using formal methods helps provide the high level of assurance required in safety-critical domains. We propose a formalization methodology relying on state-machine models and on a library of commonly applicable properties. A case study has shown that rigorous and a detailed verification of nontrivial scheduling results can be performed within reasonable time limits, using modern theorem-proving tools such as PVS. It is still necessary to develop and extend such verification efforts to the increasingly complex scheduling algorithms that may one day be used in safety-critical applications. Other aspects relevant to the avionics domain remain insufficiently explored by the formal methods community. For example, little has been done in the analysis of distributed real-time systems, where difficult problems mixing communication, processing, fault tolerance must be addressed. Formal methods are especially valuable in such complex settings, where informal proofs guided by intuition are insufficient and where other validation approaches such as testing are incomplete. Formal methods should become an essential tool for validating the most critical aspects of real-time systems, such as the partitioning mechanisms required for fault isolation in integrated avionics. Real-time scheduling problems are an ideal application area for formal methods since they are subtle and complex, must be certified to the highest degrees of assurance for supporting critical applications, and thus require very precise, detailed, and rigorous verification