欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
提出了基于命题投影时序逻辑（propositional projection temporal logic，简称PPTL）的单调速率调度（rate monotonic scheduling，简称RMs）模型检测方法．该方法使用SPIN模型检测器的系统建模语言PROMELA为任务调度系统建模，使用PPTL描述系统期望的性质，通过SPIN验证系统模型是否满足性质，从而得知一个任务组在RMS下是否可调度．同时，RMS算法控制下的任务调度系统的其他性质也可以得到验证．
英文摘要：
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.
同期刊论文项目
同项目期刊论文
位置：