An exact schedulability test for real-time systems with abstract scheduler on multiprocessor platforms

N. O. Garanina

Modelirovanie i analiz informacionnyh sistem, Tome 31 (2024) no. 4, pp. 474-494.

Résumé

This paper uses the model checking method for an exact schedulability test of real-time systems running on multiprocessor platforms. To use this method, we formally describe real-time systems with an abstract scheduler as Kripke models. This formalization provides terms sufficient to specialize the abstract scheduler. We illustrate our approach by explicitly defining schedulers that take into account preemption/non-preemption of tasks and global fixed or earliest-deadline-first priority in various combinations. The safety (schedulability) property of real-time systems is formulated using linear temporal logic LTL. Formalizing real-time systems as Kripke models and specifying the safety (schedulability) property as an LTL formula allows us to reduce the exact schedulability test of such systems to a model checking problem. We validate this approach to an exact schedulability test by implementing our formalization of real-time systems with non-preemptive global fixed-priority (NP-GFP), preemptive global fixed-priority (P-GFP), non-preemptive earliest-deadline-first priority (NP-EDF), and preemptive earliest-deadline-first priority (P-EDF) schedulers in Promela, the input language of the model checking tool SPIN. We conduct experiments in SPIN to prove/disprove the safety (schedulability) property to evaluate the effectiveness of our approach. We propose a heuristic assessment of the schedulability of a real-time system based on the provability of unsafety and unprovability of safety of a real-time system executed on multiprocessor platforms with the number of processors differing by one.

Détail

Keywords: real-time systems, exact schedulability test, Kripke models, model checking, SPIN.
Mots-clés : Promela

Bibliographie

[1] J. W. S. Liu, Real-time systems, Prentice-Hall, 2001

[2] B. B. Brandenburg, M. Gül, “Global scheduling not required: Simple, near-optimal multiprocessor real-time scheduling with semi-partitioned reservations”, Proceedings of the IEEE Real-Time Systems Symposium (RTSS), 2016, 99–110 | DOI

[3] Q. Zhou, G.Li, C. Zhou, J.Li, “Limited busy periods in response time analysis for tasks under global EDF scheduling”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 40:2 (2021), 232–245 | DOI

[4] A. Burmyakov, E. Bini, E. Tovar, “An exact schedulability test for global FP using state space pruning”, Proceedings of the 23rd International Conference on Real Time and Networks Systems, 2015, 225–234 | DOI

[5] A. Burmyakov, E. Bini, C. G. Lee, “Towards a tractable exact test for global multiprocessor fixed priority scheduling”, IEEE Transactions on Computers, 71:11 (2022), 2955–2967 | DOI

[6] S. Ranjha, P. Gohari, G. Nelissen, M. Nasri, “Partial-order reduction in reachability-based response-time analyses of limited-preemptive DAG tasks”, Real-Time Systems, 59:2 (2023), 201–255 | DOI

[7] P. Gohari, J. Voeten, M. Nasri, “Reachability-based response-time analysis of preemptive tasks underglobal scheduling”, Proceedings of the 36th Euromicro Conference on Real-Time Systems (ECRTS 2024), 2024, 3:1–3:24 | DOI

[8] Y. Sun, G. Lipari, “A pre-order relation for exact schedulability test of sporadic tasks on multiprocessor Global Fixed-Priority scheduling”, Real-Time Systems, 52:3 (2016), 323–355 | DOI | Zbl

[9] A. M.K. Cheng, Real-Time Systems: Scheduling, Analysis, and Verification, John Wiley Sons, 2002

[10] E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem et al, Handbook of model checking, 10, Springer, 2018 | MR

[11] G. J. Holzmann, The SPIN Model Checker, Primer and Reference Manual, Addison-Wesley, Reading, Massachusetts, 2003, 608 pp.

[12] R. Cavada et al, “The nuXmv symbolic model checker”, Computer Aided Verification, 2014, 334–342 | DOI

[13] N. Guan, Z. Gu, Q. Deng, S. Gao, G. Yu, “Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking”, Software Technologies for Embedded and Ubiquitous Systems, 2007, 263–272 | DOI

[14] B. Yalcinkaya, M. Nasri, B. B. Brandenburg, “An exact schedulability test for non-preemptive self-suspending real-time tasks”, Proceedings of the Design, Automation Test in Europe Conference Exhibition (DATE), 2019, 1228–1233 | DOI

[15] S. M. Staroletov, “A formal model of a partitioned real-time operating system in Promela”, Proceedings of the Institute for System Programming of the RAS, 32:6 (2020), 49–65 (in Russian) | DOI

[16] Sukvanich Punwess, Thongtak Arthit, Vatanawood Wiwat, “Formalizing real-time embedded system into Promela”, MATEC Web of Conferences, 35 (2015), 03003 | DOI

[17] G. Geeraerts, J. Goossens, T. V. A. Nguyen, “A backward algorithm for the multiprocessor online feasibility of sporadic tasks”, Proceedings of the 17th International Conference on Application of Concurrency to System Design (ACSD), 2017, 116–125 | DOI

[18] E. M. Clarke, E. A. Emerson, A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications”, ACM Transactions on Programming Languages and Systems (TOPLAS), 8:2 (1986), 244–263 | DOI | Zbl

[19] V. Bonifaci, A. Marchetti-Spaccamela, “Feasibility analysis of sporadic real-time multiprocessor task systems”, Algorithmica, 63 (2010), 763–780 | DOI | MR

[20] C. A. R. Hoare, “Communicating sequential processes”, Communications of the ACM, 21:8 (1978), 666–677 | DOI | MR | Zbl

[21] N. O. Garanina, “Anexactschedulability test for real-time systems with an abstract scheduler”, System Informatics, 25 (2024), 29–38 | DOI