maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2024-4-474-494mais-1899Research ArticleTheory of ComputingТочный тест планируемости для систем реального времени с абстрактным планировщиком на мультипроцессорных платформахAn Exact Schedulability Test for Real-Time Systems with Abstract Scheduler on Multiprocessor Platformshttps://orcid.org/0000-0001-9734-3808ГаранинаНаталья ОлеговнаGaraninaNatalia O.garanina@iis.nsk.suИнститут автоматики и электрометрии СО РАНРоссияInstitute of Automation and Electrometry SB RASRussian Federation202413122024314474494Copyright © Гаранина Н.О., 20242024Гаранина Н.О.Garanina N.O.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1899

Эта статья посвящена использованию метода верификации моделей для точного теста планируемости систем реального времени, выполняющихся на мультипроцессорных платформах. Чтобы использовать этот метод, мы формально описываем системы реального времени с абстрактным планировщиком, используя модели Крипке. Эта формализация содержит термины, достаточные для специализации абстрактного планировщика. Мы иллюстрируем наш подход, явно определяя планировщики, которые учитывают вытеснение/невытеснение задач и глобальный фиксированный приоритет или приоритет ближайшего дедлайна в различных сочетаниях. Свойство безопасности (планируемости) систем реального времени сформулировано с помощью линейной темпоральной логики LTL. Формализация систем реального времени как моделей Крипке и задание свойства безопасности (планируемости) как формулы LTL позволяет свести точный тест планируемости таких систем к задаче верификации моделей. Мы апробируем этот подход к точному тесту планируемости, реализуя на Promela — входном языке инструмента верификации моделей SPIN — нашу формализацию систем реального времени с невытесняющим планировщиком с глобальным фиксированным приоритетом (NP-GFP), вытесняющим планировщиком с глобальным фиксированным приоритетом (P-GFP), невытесняющим планировщиком с приоритетом ближайшего дедлайна (NP-EDF) и вытесняющим планировщиком с приоритетом ближайшего дедлайна (P-EDF). Мы проводим эксперименты в SPIN для доказательства/опровержения свойства безопасности (планируемости), чтобы оценить эффективность нашего подхода. Мы предлагаем эвристическую оценку планируемости системы реального времени на основе доказуемости небезопасности и недоказуемости безопасности системы реального времени при выполнении на мультипроцессорных платформах с числом процессоров, отличающимся на единицу.

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.

системы реального времениточный тест на планируемостьмодели Крипкепроверка моделейPromelaSPINreal-time systemsexact schedulability testKripke modelsmodel checkingPromelaSPINReferencesJ. W. S. Liu, Real-time systems. Prentice-Hall, 2001.J. W. S. Liu, Real-time systems. Prentice-Hall, 2001.B. B. Brandenburg and M. Gül, “Global Scheduling Not Required: Simple, Near-Optimal Multiprocessor Real-Time Scheduling with Semi-Partitioned Reservations,” in Proceedings of the IEEE Real-Time Systems Symposium (RTSS), 2016, pp. 99–110, doi: 10.1109/RTSS.2016.019.B. B. Brandenburg and M. Gül, “Global Scheduling Not Required: Simple, Near-Optimal Multiprocessor Real-Time Scheduling with Semi-Partitioned Reservations,” in Proceedings of the IEEE Real-Time Systems Symposium (RTSS), 2016, pp. 99–110, doi: 10.1109/RTSS.2016.019.Q. Zhou, G. Li, C. Zhou, and 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, vol. 40, no. 2, pp. 232–245, 2021, doi: 10.1109/TCAD.2020.2994265.Q. Zhou, G. Li, C. Zhou, and 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, vol. 40, no. 2, pp. 232–245, 2021, doi: 10.1109/TCAD.2020.2994265.A. Burmyakov, E. Bini, and E. Tovar, “An exact schedulability test for global FP using state space pruning,” in Proceedings of the 23rd International Conference on Real Time and Networks Systems, 2015, pp. 225–234, doi: 10.1145/2834848.2834877.A. Burmyakov, E. Bini, and E. Tovar, “An exact schedulability test for global FP using state space pruning,” in Proceedings of the 23rd International Conference on Real Time and Networks Systems, 2015, pp. 225–234, doi: 10.1145/2834848.2834877.A. Burmyakov, E. Bini, and C.-G. Lee, “Towards a Tractable Exact Test for Global Multiprocessor Fixed Priority Scheduling,” IEEE Transactions on Computers, vol. 71, no. 11, pp. 2955–2967, 2022, doi: 10.1109/TC.2022.3142540.A. Burmyakov, E. Bini, and C.-G. Lee, “Towards a Tractable Exact Test for Global Multiprocessor Fixed Priority Scheduling,” IEEE Transactions on Computers, vol. 71, no. 11, pp. 2955–2967, 2022, doi: 10.1109/TC.2022.3142540.S. Ranjha, P. Gohari, G. Nelissen, and M. Nasri, “Partial-order reduction in reachability-based response-time analyses of limited-preemptive DAG tasks,” Real-Time Systems, vol. 59, no. 2, pp. 201–255, 2023, doi: 10.1007/s11241-023-09398-x.S. Ranjha, P. Gohari, G. Nelissen, and M. Nasri, “Partial-order reduction in reachability-based response-time analyses of limited-preemptive DAG tasks,” Real-Time Systems, vol. 59, no. 2, pp. 201–255, 2023, doi: 10.1007/s11241-023-09398-x.P. Gohari, J. Voeten, and M. Nasri, “Reachability-Based Response-Time Analysis of Preemptive Tasks Under Global Scheduling,” in Proceedings of the 36th Euromicro Conference on Real-Time Systems (ECRTS 2024), 2024, pp. 3:1–3:24, doi: 10.4230/LIPIcs.ECRTS.2024.3.P. Gohari, J. Voeten, and M. Nasri, “Reachability-Based Response-Time Analysis of Preemptive Tasks Under Global Scheduling,” in Proceedings of the 36th Euromicro Conference on Real-Time Systems (ECRTS 2024), 2024, pp. 3:1–3:24, doi: 10.4230/LIPIcs.ECRTS.2024.3.Y. Sun and G. Lipari, “A pre-order relation for exact schedulability test of sporadic tasks on multiprocessor Global Fixed-Priority scheduling,” Real-Time Systems, vol. 52, no. 3, pp. 323–355, 2016, doi: 10.1007/s11241-015-9245-9.Y. Sun and G. Lipari, “A pre-order relation for exact schedulability test of sporadic tasks on multiprocessor Global Fixed-Priority scheduling,” Real-Time Systems, vol. 52, no. 3, pp. 323–355, 2016, doi: 10.1007/s11241-015-9245-9.A. M. K. Cheng, Real‐Time Systems: Scheduling, Analysis, and Verification. John Wiley & Sons, 2002.A. M. K. Cheng, Real‐Time Systems: Scheduling, Analysis, and Verification. John Wiley & Sons, 2002.E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, and others, Handbook of model checking, vol. 10. Springer, 2018.E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, and others, Handbook of model checking, vol. 10. Springer, 2018.G. J. Holzmann, The SPIN Model Checker, Primer and Reference Manual. Addison-Wesley, Reading, Massachusetts, 2003.G. J. Holzmann, The SPIN Model Checker, Primer and Reference Manual. Addison-Wesley, Reading, Massachusetts, 2003.R. Cavada et al., “The nuXmv Symbolic Model Checker,” in Computer Aided Verification, 2014, pp. 334–342, doi: 10.1007/978-3-319-08867-9_22.R. Cavada et al., “The nuXmv Symbolic Model Checker,” in Computer Aided Verification, 2014, pp. 334–342, doi: 10.1007/978-3-319-08867-9_22.N. Guan, Z. Gu, Q. Deng, S. Gao, and G. Yu, “Exact Schedulability Analysis for Static-Priority Global Multiprocessor Scheduling Using Model-Checking,” in Software Technologies for Embedded and Ubiquitous Systems, 2007, pp. 263–272.N. Guan, Z. Gu, Q. Deng, S. Gao, and G. Yu, “Exact Schedulability Analysis for Static-Priority Global Multiprocessor Scheduling Using Model-Checking,” in Software Technologies for Embedded and Ubiquitous Systems, 2007, pp. 263–272.B. Yalcinkaya, M. Nasri, and B. B. Brandenburg, “An Exact Schedulability Test for Non-Preemptive Self-Suspending Real-Time Tasks,” in Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE), 2019, pp. 1228–1233, doi: 10.23919/DATE.2019.8715111.B. Yalcinkaya, M. Nasri, and B. B. Brandenburg, “An Exact Schedulability Test for Non-Preemptive Self-Suspending Real-Time Tasks,” in Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE), 2019, pp. 1228–1233, doi: 10.23919/DATE.2019.8715111.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, vol. 32, no. 6, pp. 49–65, 2020.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, vol. 32, no. 6, pp. 49–65, 2020.Sukvanich, Punwess, Thongtak, Arthit, and Vatanawood, Wiwat, “Formalizing Real-Time Embedded System into Promela,” MATEC Web of Conferences, vol. 35, p. 03003, 2015, doi: 10.1051/matecconf/20153503003.Sukvanich, Punwess, Thongtak, Arthit, and Vatanawood, Wiwat, “Formalizing Real-Time Embedded System into Promela,” MATEC Web of Conferences, vol. 35, p. 03003, 2015, doi: 10.1051/matecconf/20153503003.G. Geeraerts, J. Goossens, and T.-V.-A. Nguyen, “A Backward Algorithm for the Multiprocessor Online Feasibility of Sporadic Tasks,” in Proceedings of the 17th International Conference on Application of Concurrency to System Design (ACSD), 2017, pp. 116–125, doi: 10.1109/ACSD.2017.9.G. Geeraerts, J. Goossens, and T.-V.-A. Nguyen, “A Backward Algorithm for the Multiprocessor Online Feasibility of Sporadic Tasks,” in Proceedings of the 17th International Conference on Application of Concurrency to System Design (ACSD), 2017, pp. 116–125, doi: 10.1109/ACSD.2017.9.E. M. Clarke, E. A. Emerson, and A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 8, no. 2, pp. 244–263, 1986.E. M. Clarke, E. A. Emerson, and A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 8, no. 2, pp. 244–263, 1986.V. Bonifaci and A. Marchetti-Spaccamela, “Feasibility Analysis of Sporadic Real-Time Multiprocessor Task Systems,” Algorithmica, vol. 63, pp. 763–780, 2010.V. Bonifaci and A. Marchetti-Spaccamela, “Feasibility Analysis of Sporadic Real-Time Multiprocessor Task Systems,” Algorithmica, vol. 63, pp. 763–780, 2010.C. A. R. Hoare, “Communicating sequential processes,” Communications of the ACM, vol. 21, no. 8, pp. 666–677, 1978.C. A. R. Hoare, “Communicating sequential processes,” Communications of the ACM, vol. 21, no. 8, pp. 666–677, 1978.N. O. Garanina, “An Exact Schedulability Test for Real-time Systems with an Abstract Scheduler,” System Informatics, vol. 25, pp. 29–38, 2024, doi: 10.31144/si.2307-6410.2024.n25.p29-38.N. O. Garanina, “An Exact Schedulability Test for Real-time Systems with an Abstract Scheduler,” System Informatics, vol. 25, pp. 29–38, 2024, doi: 10.31144/si.2307-6410.2024.n25.p29-38.

The authors declare that there are no conflicts of interest present.