Model Checking Rate-Monotonic Scheduler with TMSVL

This paper presents a model checking-based schedulability checking approach for Rate-Monotonic Scheduling (RMS) algorithm. To do so, RMS algorithm is modelled with TMSVL, and the desired property, i.e. Schedulability, is specified with the property specification language in TMSVL. Next, whether RMS algorithm is schedulable on a set of tasks is verified by checking whether the desired property is valid on the TMSVL model. A significant advantage of TMSVL is the mechanism of adjustable time intervals which makes an effective reduction on the state space.