A model-checking approach to schedulability analysis of global multiprocessor scheduling with fixed offsets

It is an active research topic to determine schedulability of a real-time sporadic or periodic taskset on a multicore processor with global scheduling policies such as global fixed-priority (FP) or earliest deadline first (EDF) algorithms. Analytical techniques such as utilisation bound tests and response time analysis algorithms generally suffer from excessive pessimism, and may cause low system utilisation. In this paper, we apply model-checking to address the restricted task model of periodic tasks with fixed release offsets and possible release jitter. We believe that this restricted task model is more realistic for current industry practice than the more general sporadic task model, since it can achieve higher CPU utilisation and better predicability. We present an approach to schedulability analysis of this restricted task model using the timed automata model-checker UPPAAL. This modelling framework is flexible and expressive, and can achieve reasonable scalability.