Title :
Schedulability Analysis of Global Fixed-Priority or EDF Multiprocessor Scheduling with Symbolic Model-Checking
Author :
Guan, Nan ; Gu, Zonghua ; Lv, Mingsong ; Deng, Qingxu ; Yu, Ge
Author_Institution :
Dept. of Comput. Sci. & Technol., Northeastern Univ., Shenyang
Abstract :
As Moore´s law comes to an end, multi-processor (MP) systems are becoming increasingly important in embedded systems design, hence real-time schedulability analysis for MP systems has become an important research topic. In this paper, we present an exact method for schedulability analysis of global multiprocessor scheduling with either fixed-priority (FP) or earliest-deadline-first (EDF) algorithms using the model-checker NuSMV. Compared to safe but pessimistic schedulability tests based on processor utilization bounds, model-checking can provide an exact answer to the schedulability of a taskset, as well as quantitative information on each task´s best-case and worst- case response times.
Keywords :
formal verification; processor scheduling; EDF multiprocessor scheduling; FP scheduling; MP systems; NuSMV model-checker; fixed-priority multiprocessor scheduling; global multiprocessor scheduling; real-time schedulability analysis; symbolic model-checking; Algorithm design and analysis; Computer science; Delay; Embedded system; Moore´s Law; Object oriented modeling; Processor scheduling; Real time systems; Scheduling algorithm; State-space methods; Schedulability; real-time scheduling; symbolic model-checking;
Conference_Titel :
Object Oriented Real-Time Distributed Computing (ISORC), 2008 11th IEEE International Symposium on
Conference_Location :
Orlando, FL
Print_ISBN :
978-0-7695-3132-8
DOI :
10.1109/ISORC.2008.74
