Int J Performability Eng ›› 2017, Vol. 13 ›› Issue (6): 785-795.doi: 10.23940/ijpe.17.06.p1.785795

• Original articles •     Next Articles

Schedulability Analysis and Symbolic Verification Method for Heterogeneous Multicore Real-Time Systems

Wei Wang*, Zhengyu Liao, Dong Guo, Hui Zhang, Chunqi Tian, and Jianing Tong   

  1. Department of computer science and technology, Tongji University, Shanghai 200092, China

Abstract: As heterogeneous multicore real-time systems are increasingly applied in safety critical systems, it is important to ensure the correctness of these systems. One key attribute of real-time systems is the schedulability that guarantees to satisfy the timing requirements. This paper presents a method for modeling and verifying schedulability of heterogeneous multi-core systems and the method we present uses timed-automata (TA) to model tasks and resources of heterogeneous systems considering their special features. Also this method allows us to establish complex dependences between tasks and use different scheduling policies. After that we choose CPU-GPU heterogeneous multi-core systems as an example and we model three TA networks according to three levels of this system, which are real-time tasks, resources and scheduling management modules. Finally, we use UPPAAL to verify if the model we established satisfies habitudes. According to our method, we present a link between model checking methods and schedulability analysis method for heterogeneous multicore real-time systems and we can automatically and accurately verify the schedulability of selected systems.


Submitted on July 25, 2017; Revised on August 30, 2017; Accepted on September 15, 2017(This paper was presented at the Third International Symposium on System and Software Reliability.
References: 13