Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking
Nan Guan, Zhuoer Gu, Qian Deng, Shengli Gao, Yu Gong · 2007
Abstract — To determine schedulability of prioritydriven periodic tasksets on multi-processor systems, it is necessary to rely on utilization bound tests that are safe but pessimistic, since there is no known method for exact schedulability analysis for multi-processor systems analogous to the response time analysis algorithm for single-processor systems. In this paper, we use model-checking to provide a technique for exact multiprocessor scheduability analysis by modeling the realtime multi-tasking system with Timed Automata (TA), and transforming the schedulability analysis problem into the reachability checking problem of the TA model. I.