A Event-B-Based Approach for Schedulability Analysis For Real-Time Scheduling Algorithms through Deadlock Detection

Event-B is a refinement-based formal method that enables incremental modeling of complex systems and supports verifying system properties. Real-time systems adhere to strict timing constraints by the tasks within the system. The real-time scheduling algorithm serves as the cornerstone to guarantee the timely completion of tasks. Therefore, modeling real-time scheduling algorithms and verifying schedulability represent prominent areas of focus within the realm of real-time systems. While existing approaches often employ model checking, the scalability of the model and the problem of state explosion during verification remain challenges. Relying on theorem proving, Event-B allows for rigorous verification of system properties and circumvents state explosion. Benefiting from model refinement, the abstract model can be extended and refined to implement various scheduling algorithms. This paper introduces an Event-B-based framework for modeling real-time scheduling algorithms and verifying properties, including schedulability. The framework provides a common refinement pattern for modeling the schedulability of the Event-B model. It facilitates the transformation of the schedulability analysis on the obtained model into the deadlock detection problem within the model. Deadlock detection can be effectively addressed through either theorem proving or model checker. We utilized Event-B to model and refine several real-time scheduling algorithms. Following the formal verification of functional and environmental requirements, we analyzed and verified the model’s schedulability within the proposed framework.