Schedulability analysis and symbolic verification method for heterogeneous multicore real-time systems

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 multicore 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.