An improved formalization analysis approach to determine schedulability of global multiprocessor scheduling based on symbolic safety analysis and statistical model checking in smartphone systems

Modern smart phones are typically equipped with multicore processors. In this paper, we address the problem of determining schedulability of a real-time periodic taskset with fixed release offsets and possible release jitters on a multicore processor with global Fixed-Priority (FP) or EDF (Earliest Deadline First) scheduling algorithms, using the model-checker UPPAAL for Timed Automata. In addition to yes/no schedulability analysis for hard real-time systems, we also apply statistical model checking to estimate the probability of unschedulability for soft real-time systems, described with two statistical parameters (confidence and accuracy).