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

Authors: Zonghua Gu; Zhu Wang; Haolan Chen; Haibin Cai

Addresses: College of Computer Science, Zhejiang University, Hangzhou, 310027, China ' College of Computer Science, Zhejiang University, Hangzhou, 310027, China ' College of Computer Science, Zhejiang University, Hangzhou, 310027, China ' Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, 200062, China

Abstract: 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.

Keywords: real-time scheduling; multiprocessor scheduling; schedulability analysis; model checking; fixed offsets; multicore processors.

DOI: 10.1504/IJES.2014.063815

International Journal of Embedded Systems, 2014 Vol.6 No.2/3, pp.176 - 187

Received: 20 Sep 2013
Accepted: 11 Oct 2013
Published online: 31 Jul 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article