PROBABILISTIC FORMAL MODELING AND VERIFICATION OF REAL TIME TASK SCHEDULING ON MULTIPROCESSOR SYSTEMS

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.