Точный тест планируемости для систем реального времени с абстрактным планировщиком на мультипроцессорных платформах

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

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

2. 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.

3. 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.

4. 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.

5. 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.

6. 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.

7. 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.

8. 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.

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, and others, Handbook of model checking, vol. 10. Springer, 2018.

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

12. 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.

13. 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.

14. 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.

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, vol. 32, no. 6, pp. 49–65, 2020.

16. 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.

17. 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.

18. 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.

19. V. Bonifaci and A. Marchetti-Spaccamela, “Feasibility Analysis of Sporadic Real-Time Multiprocessor Task Systems,” Algorithmica, vol. 63, pp. 763–780, 2010.

20. C. A. R. Hoare, “Communicating sequential processes,” Communications of the ACM, vol. 21, no. 8, pp. 666–677, 1978.

21. 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.