基于命题投影时序逻辑的单调速率调度算法模型检测

• 作者: 段振华 田聪
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 时序逻辑 模型检测 单调速率调度算法 验证 实时系统
• 年，卷（期）: 2011,（2）
• 所属期刊栏目: 系统软件与软件工程
• 页码范围: 211-221
• 分类号: TP311
• 字数: 6659字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2011.03729

摘要

提出了基于命题投影时序逻辑(propositional projection temporal logic,简称PPTL)的单调速率调度(rate monotonic scheduling,简称RMS)模型检测方法.该方法使用SPIN模型检测器的系统建模语言PROMELA为任务调度系统建模,使用PPTL描述系统期望的性质,通过SPIN验证系统模型是否满足性质,从而得知一个任务组在RMS下是否可调度.同时,RMS算法控制下的任务调度系统的其他性质也可以得到验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	段振华	西安电子科技大学计算理论与技术研究所	47	363	10.0	16.0
5	田聪	西安电子科技大学计算理论与技术研究所	8	41	4.0	6.0