Model checking timed systems with priorities

Priorities are used to resolve conflicts such as in re-source sharing and in safety designs. The use of priorities has become indispensable in real-time system design such as in scheduling, synchronization, arbitration, and fairness guaranteeing. There are several modeling frameworks that show how timed systems with priorities are to be designed and how priority schedulers can be automatically synthesized. However, the verification of timed systems with priorities using model checking is still a relatively untouched area. We show what the issues are in model checking timed systems with priorities and how the issues are solved in this work. In the process, we propose an optimal zone subtraction algorithm. The method has been implemented into the SGM model checker and successfully applied to real-time embedded systems and safety-critical systems, which illustrate the feasibility and advantages of the proposed verification method.