利用投影时序逻辑的多内核进程调度建模与验证

• 作者: 段振华 舒新峰
• 来源期刊: 西安交通大学学报
• 关键词: 投影时序逻辑 进程调度 定理证明 多核处理器 调度验证
• 年，卷（期）: 2010,（3）
• 页码范围: 52-57
• 页数: 6页
• 分类号: TP301
• 语种: 中文

摘要

针对软件测试无法满足多内核处理器上进程调度的验证需要这一问题,提出利用投影时序逻辑(PTL)的定理证明方法来验证进程调度.使用PTL公式建立了支持当前主流进程调度算法的多内核处理器进程调度一般模型S,并将系统期望的性质描述为PTL公式P,在PTL公理系统的基础上,通过证明S蕴含P是否为一个定理来验证系统是否具备该性质.以2内核处理器上的多级反馈队列算法的正确性为案例进行检验,结果表明所提方法可验证多内核处理器进程调度的系统性质,保证多内核进程调度的可靠性.由于多内核处理器的进程调度具备了并发系统的主要特点,因此该方法也适用于一般的并发系统验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	段振华	西安电子科技大学计算理论与技术研究所	47	363	10.0	16.0
2	舒新峰	西安电子科技大学计算理论与技术研究所	3	11	2.0	3.0