Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-b. Int. J. Softw. Tools Technol. Transf. 12, 447–466 (2010)
Abrial, J.R., Hoare, A., Chapron, P.: The b-book. (No Title) (1996)
Butler, M., Falampin, J.: An approach to modelling and refining timing properties in b (2002)
Cansell, D., Méry, D., Rehm, J.: Time constraint patterns for event B development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 140–154. Springer, Heidelberg (2006). https://doi.org/10.1007/11955757_13
David, A., Illum, J., Larsen, K.G., Skou, A.: Model-based framework for schedulability analysis using UPPAAL 4.1. In: Model-Based Design for Embedded Systems, pp. 117–144. CRC Press (2018)
Foughali, M., Hladik, P.E.: Bridging the gap between formal verification and schedulability analysis: the case of robotics. J. Syst. Archit. 111, 101817 (2020)
Guan, N., Gu, Z., Deng, Q., Gao, S., Yu, G.: Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking. In: Obermaisser, R., Nah, Y., Puschner, P., Rammig, F.J. (eds.) SEUS 2007. LNCS, vol. 4761, pp. 263–272. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75664-4_26
Haur, I., Béchennec, J.L., Roux, O.H.: Formal schedulability analysis based on multi-core RTOS model. In: 29th International Conference on Real-Time Networks and Systems, pp. 216–225 (2021)
Leuschel, M., Butler, M.: ProB: a model checker for b. In: FME 2003: Formal Methods: International Symposium of Formal Methods Europe, Pisa, Italy, 8–14 September 2003. Proceedings, LNCS, pp. 855–874. Springer, Berlin, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46
Liu, C.L., Layland, J.W.: Scheduling algorithms for multiprogramming in a hard-real-time environment. J. ACM (JACM) 20(1), 46–61 (1973)
Rehm, J.: From absolute-timer to relative-countdown: patterns for model-checking (2008)
Sarshogh, M.R., Butler, M.: Specification and refinement of discrete timing properties in event-b (2011)
Sha, L., Lehoczky, J.P., Rajkumar, R.: Solutions for some practical problems in prioritized preemptive scheduling, pp. 181–191. IEEE (1986). In: Unknown Host Publication Title
Sprunt, B., Sha, L., Lehoczky, J.: Aperiodic task scheduling for hard-real-time systems. Real-Time Syst. 1, 27–60 (1989)
Strosnider, J.K., Lehoczky, J.P., Sha, L.: The deferrable server algorithm for enhanced aperiodic responsiveness in hard real-time environments. IEEE Trans. Comput. 44(1), 73–91 (1995)
Sulskus, G., Poppleton, M., Rezazadeh, A.: An interval-based approach to modelling time in Event-B. In: Dastani, M., Sirjani, M. (eds.) FSEN 2015. LNCS, vol. 9392, pp. 292–307. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24644-4_20
Waszniowski, L., Hanzálek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38, 39–65 (2008)
Zhu, C., Butler, M., Cirstea, C.: Refinement of timing constraints for concurrent tasks with scheduling. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 219–233. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4_15
Acknowledgments
This work is supported by the National Key Research and Development Program (2022YFB3305200), the National Natural Science Foundation of China NSFC (No. 92370201, No. 62272165), the “Digital Silk Road” Shanghai International Joint Lab of Trustworthy Intelligent Software (No. 22510750100) and Shanghai Trusted Industry Internet Software Collaborative Innovation Center.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Quan, J., Li, Q. (2025). A Event-B-Based Approach for Schedulability Analysis For Real-Time Scheduling Algorithms through Deadlock Detection. In: Bai, G., Ishikawa, F., Ait-Ameur, Y., Papadopoulos, G.A. (eds) Engineering of Complex Computer Systems. ICECCS 2024. Lecture Notes in Computer Science, vol 14784 . Springer, Cham. https://doi.org/10.1007/978-3-031-66456-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-031-66456-4_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-66455-7
Online ISBN: 978-3-031-66456-4
eBook Packages: Computer ScienceComputer Science (R0)