An Exact Schedulability Test for Real-Time Systems with Abstract Scheduler on Multiprocessor Platforms

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.

real-time systems, exact schedulability test, Kripke models, model checking, Promela, 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.