Geodesic
An exact schedulability test for real-time systems with abstract scheduler on multiprocessor platforms
Modelirovanie i analiz informacionnyh sistem, Tome 31 (2024) no. 4, pp. 474-494

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: real-time systems, exact schedulability test, Kripke models, model checking, SPIN.
Mots-clés : Promela 
@article{MAIS_2024_31_4_a4,
     author = {N. O. Garanina},
     title = {An exact schedulability test for real-time systems with abstract scheduler on multiprocessor platforms},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {474--494},
     publisher = {mathdoc},
     volume = {31},
     number = {4},
     year = {2024},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2024_31_4_a4/}
}
TY  - JOUR
AU  - N. O. Garanina
TI  - An exact schedulability test for real-time systems with abstract scheduler on multiprocessor platforms
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2024
SP  - 474
EP  - 494
VL  - 31
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2024_31_4_a4/
LA  - ru
ID  - MAIS_2024_31_4_a4
ER  - 
%0 Journal Article
%A N. O. Garanina
%T An exact schedulability test for real-time systems with abstract scheduler on multiprocessor platforms
%J Modelirovanie i analiz informacionnyh sistem
%D 2024
%P 474-494
%V 31
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2024_31_4_a4/
%G ru
%F MAIS_2024_31_4_a4
N. O. Garanina. An exact schedulability test for real-time systems with abstract scheduler on multiprocessor platforms. Modelirovanie i analiz informacionnyh sistem, Tome 31 (2024) no. 4, pp. 474-494. http://geodesic.mathdoc.fr/item/MAIS_2024_31_4_a4/