A model-checking approach to schedulability analysis of global multiprocessor scheduling with fixed offsets. (1st January 2014)

• Record Type: Journal Article
• Authors: Gu, Zonghua; Wang, Zhu; Chen, Haolan; Cai, Haibin
• Is Part Of: International journal of embedded systems. Volume 6:Number 2/3(2014)
• Page Start: 176
• Page End: 187
• Publication Date: 2014-01-01
• Subjects: real-time scheduling -- multiprocessor scheduling -- schedulability analysis -- model-checking; Embedded computer systems -- Periodicals; 004.16
• Languages: English
• ISSNs: 1741-1068

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.