%0 Journal Article
%T Model Checking Rate Monotonic Scheduling Algorithm Based on Propositional Projection Temporal Logic<br>基于命题投影时序逻辑的单调速率调度算法模型检测
%A TIAN Cong
%A DUAN Zhen-Hua
%A <br>田聪
%A 段振华
%J 软件学报
%D 2011
%I 
%X A propositional projection temporal logic (PPTL) based model checking approach for rate monotonic scheduling (RMS) is presented. With this approach, RMS controlled systems are modeled by PROMELA, which is the system modeling language in model checker SPIN. The desired property is specified by a PPTL formula. Next, whether or not the system satisfies the property can be verified with SPIN. Accordingly, the schedulability of a group of tasks can be obtained; meanwhile, other properties of the tasks scheduling system under RMS algorithm can also be verified.
%K temporal logic
%K model checking
%K rate monotonic scheduling algorithm
%K verification
%K real time system<br>时序逻辑
%K 模型检测
%K 单调速率调度算法
%K 验证
%K 实时系统
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=3D6AC17FA29F6E99E7B7046AC86F4CC1&yid=9377ED8094509821&vid=BC12EA701C895178&iid=0B39A22176CE99FB&sid=CC0ECB9C52F1B85F&eid=78F0EFE028BD3783&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=19