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...
Saved in:
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2024-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1899 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849241024626425856 |
|---|---|
| author | Natalia O. Garanina |
| author_facet | Natalia O. Garanina |
| author_sort | Natalia O. Garanina |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-3aaf2e434851496eaeb7c61c2db08ae2 |
| institution | Kabale University |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2024-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-3aaf2e434851496eaeb7c61c2db08ae22025-08-20T04:00:19ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172024-12-0131447449410.18255/1818-1015-2024-4-474-4941423An Exact Schedulability Test for Real-Time Systems with Abstract Scheduler on Multiprocessor PlatformsNatalia O. Garanina0Institute of Automation and Electrometry SB RASThis 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.https://www.mais-journal.ru/jour/article/view/1899real-time systemsexact schedulability testkripke modelsmodel checkingpromelaspin |
| spellingShingle | Natalia O. Garanina An Exact Schedulability Test for Real-Time Systems with Abstract Scheduler on Multiprocessor Platforms Моделирование и анализ информационных систем real-time systems exact schedulability test kripke models model checking promela spin |
| title | An Exact Schedulability Test for Real-Time Systems with Abstract Scheduler on Multiprocessor Platforms |
| title_full | An Exact Schedulability Test for Real-Time Systems with Abstract Scheduler on Multiprocessor Platforms |
| title_fullStr | An Exact Schedulability Test for Real-Time Systems with Abstract Scheduler on Multiprocessor Platforms |
| title_full_unstemmed | An Exact Schedulability Test for Real-Time Systems with Abstract Scheduler on Multiprocessor Platforms |
| title_short | An Exact Schedulability Test for Real-Time Systems with Abstract Scheduler on Multiprocessor Platforms |
| title_sort | exact schedulability test for real time systems with abstract scheduler on multiprocessor platforms |
| topic | real-time systems exact schedulability test kripke models model checking promela spin |
| url | https://www.mais-journal.ru/jour/article/view/1899 |
| work_keys_str_mv | AT nataliaogaranina anexactschedulabilitytestforrealtimesystemswithabstractscheduleronmultiprocessorplatforms AT nataliaogaranina exactschedulabilitytestforrealtimesystemswithabstractscheduleronmultiprocessorplatforms |