A Resource Scheduling Design Method with Model Checking for Distributed Embedded Software

In this paper, we deal with the kind of distributed embedded software that is constructed from tasks that communicate with each other by sending and receiving multicast messages. These tasks must share resources. So, it is important to schedule a timetable describing when the tasks occupy the resources so that there is no resource competition and the tasks occupy the resources within pre-specified periods. We call this scheduling process resource scheduling. Because tasks must satisfy many constraints and there are message delays in the communication of the tasks, resource scheduling is a difficult task. So, resource scheduling design methods are necessary. In this paper, we propose a resource scheduling design method that allows multicast messages whose receivers can be more than three tasks and an efficient verification method for the method.