摘要

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).