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.
Index Terms:
Schedulability, real-time scheduling, symbolic model-checking
Citation:
Nan Guan, Zonghua Gu, Mingsong Lv, Qingxu Deng, Ge Yu, "Schedulability Analysis of Global Fixed-Priority or EDF Multiprocessor Scheduling with Symbolic Model-Checking," isorc, pp.556-560, 2008 11th IEEE Symposium on Object Oriented Real-Time Distributed Computing (ISORC), 2008