| 基于命题投影时序逻辑的单调速率调度算法模型检测 |
| |
| 引用本文： | 田聪,段振华.基于命题投影时序逻辑的单调速率调度算法模型检测[J].软件学报,2011,22(2):211-221. |
| |
| 作者姓名： | 田聪 段振华 |
| |
| 作者单位： | 西安电子科技大学计算理论与技术研究所,陕西西安710071;西安电子科技大学综合业务网理论及关键技术国家重点实验室,陕西西安710071 |
| |
| 基金项目： | 国家自然科学基金(61003078, 91018010, 60873018, 60910004); 国家重点基础研究发展计划(973)(2010CB328102);教育部博士点基金(200807010012); 中央高校基本科研业务费专项资金(JY10000903004) |
| |
| 摘 要： | 提出了基于命题投影时序逻辑(propositional projection temporal logic,简称PPTL)的单调速率调度(rate monotonic scheduling,简称RMS)模型检测方法.该方法使用SPIN模型检测器的系统建模语言PROMELA为任务调度系统建模,使用PPTL描述系统期望的性质,通过SPIN验证系统模型是否满足性质,从而得知一个任务组在RMS下是否可调度.同时,RMS算法控制下的任务调度系统的其他性质也可以得到验证.
|
| 关 键 词： | 时序逻辑 模型检测 单调速率调度算法 验证 实时系统 |
| 收稿时间： | 2008/12/24 0:00:00 |
| 修稿时间： | 6/9/2009 12:00:00 AM |
Model Checking Rate Monotonic Scheduling Algorithm Based on Propositional Projection Temporal Logic |
| |
| TIAN Cong and DUAN Zhen-Hua.Model Checking Rate Monotonic Scheduling Algorithm Based on Propositional Projection Temporal Logic[J].Journal of Software,2011,22(2):211-221. |
| |
| Authors: | TIAN Cong and DUAN Zhen-Hua |
| |
| Affiliation: | TIAN Cong1,2,DUAN Zhen-Hua1,2 1(Institute of Computing Theory and Technology,Xidian University,Xi'an 710071,China) 2(State Key Laboratory of Integrated Services Networks,China) |
| |
| Abstract: | 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. |
| |
| Keywords: | temporal logic model checking rate monotonic scheduling algorithm verification real time system |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
