Abstract:
The emerging multiprocessors technology is increasingly penetrating into the advanced
real-time systems which poses great challenges for job scheduling in real-time resource
management systems. An efficient and reliable scheduling analysis technique is vital
for non-deterministic tasks in safety-critical systems. This study explores state-ofthe-
art automated stochastic formal techniques for real time scheduling analysis and
verification. This is the first work so far that employs colored stochastic Petri nets
(SPNC) and probabilistic model verification based framework for multiprocessor realtime
scheduling algorithms. Stochastic Petri net (SPN) model of general job scheduler
is evaluated via simulations, structural analysis and stochastic model checking.
Specifically, this study demonstrates SPNC model of preemptive and dynamic priority
based global earliest deadline first (gEDF), a non-trivial scheduling algorithm for
real time multiprocessor environment. The underlying SPN model of SPNC and its
continuous-time Markov chain are deeply examined and validated using stochastic simulations
and model checking technique. Hence, this work suggests a framework for the
formal analysis of real time scheduling algorithms and it successfully proves to provide
a live, scalable and robust solution for gEDF scheduling algorithm. This study will further
serve as a basis to systematically analyze the real time multiprocessor scheduling
problems tremendously using probabilistic formal methods.
