Verification of a real time scheduling protocol of safety-critical systems

It is of great importance to ensure the correctness 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 the safety-critical system and models it using a Modeling, Simulation and Verification Language program. Then the sufficient and necessary conditions for the schedulability are given. Further, the schedulability and other properties are verified using the MSV toolkit.