Model Checking Rate-Monotonic Scheduler with TMSVL

Author

Jin Cui ; Zhenhua Duan ; Cong Tian

Author_Institution

ISN Lab., Xidian Univ., Xi´an, China

fYear

2014

fDate

4-7 Aug. 2014

Firstpage

202

Lastpage

205

Abstract

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.

Keywords

formal specification; formal verification; parallel programming; programming languages; scheduling; specification languages; RMS algorithm; TMSVL model; adjustable time intervals; model checking-based schedulability checking approach; parallel programming language; property specification language; rate-monotonic scheduling algorithm; state space reduction; verification; Algorithm design and analysis; Clocks; Educational institutions; Model checking; Real-time systems; Scheduling; Time factors; Rate-Monotonic Scheduler; TMSVL; model checking; real-time systems;

fLanguage

English

Publisher

ieee

Conference_Titel

Engineering of Complex Computer Systems (ICECCS), 2014 19th International Conference on

Conference_Location

Tianjin

Print_ISBN

978-1-4799-5481-0

Type

conf

DOI

10.1109/ICECCS.2014.37

Filename

6923139