An Exact Schedulability Test for Real-Time Systems with an 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/nonpreemption of tasks and global-fixed-priority 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 a nonpreemptive global-fixed-priority (NP-GFP) scheduler, preemptive global-fixed-priority (P-GFP) scheduler, nonpreemptive earliest-deadline-first (NP-EDF) priority scheduler, and preemptive earliest-deadline-first (P-EDF) priority scheduler 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.