利用投影时序逻辑的多内核进程调度建模与验证
针对软件测试无法满足多内核处理器上进程调度的验证需要这一问题,提出利用投影时序逻辑(PTL)的定理证明方法来验证进程调度.使用PTL公式建立了支持当前主流进程调度算法的多内核处理器进程调度一般模型S,并将系统期望的性质描述为PTL公式P,在PTL公理系统的基础上,通过证明S蕴含P是否为一个定理来验证系统是否具备该性质.以2内核处理器上的多级反馈队列算法的正确性为案例进行检验,结果表明所提方法可验证多内核处理器进程调度的系统性质,保证多内核进程调度的可靠性.由于多内核处理器的进程调度具备了并发系统的主要特点,因此该方法也适用于一般的并发系统验证.
投影时序逻辑、进程调度、定理证明、多核处理器、调度验证
44
TP301(计算技术、计算机技术)
国家自然科学基金资助重大国际合作项目60910004;国家"973计划"重点资助项目2010CB328102;国家自然科学基金重点资助项目60433010;国家自然科学基金资助项目60873018;总装备部预研项目51315050105
2010-05-04（万方平台首次上网日期，不代表论文的发表时间）
共6页
52-57
