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

fYear

2008

fDate

5-7 May 2008

Firstpage

556

Lastpage

560

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/ISORC.2008.74

Filename

4559587