Model Checking Techniques Enable Schedulability Analysis of Real-Time Systems

A real-time system should ensure specific timing constraints. This type of system needs to meet the deadline for its jobs. In general, the increasing lateness following how late a real-time system finishes its tasks/processes concerning the deadline may decrease the accuracy and usefulness of the system. That means violation of the deadline may cause problems for this kind of system. Thus, several scheduling policies are introduced to guide the execution of the processes. From that point, checking the schedulability for real-time systems is necessary and important. This paper presents an approach to analyzing the schedulability of real-time systems. Our method includes: First, we introduce a specification language to facilitate the description of the scheduling policies with the attributes of the processes (including the deadline for each task). Second, we consider the time taken for the tasks/processes of the system as one action taking one-time unit (using discrete time). This approach allows us to model the behaviors and realize the time taken by each action of the processes. Third, we apply model checking techniques to explore the states of the system and then check the deadline violation. The exploration is guided by the information specified in the language for the scheduling policy. The information here is generated automatically from the description of the scheduler. The experiment results show that we can handle this problem accurately and easily.