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

Modeling and Verification of Processes Scheduling Based on Projection Temporal Logic for Multi-Core CPU

作　　者：舒新峰[1] 段振华[1] 

机构地区：[1]西安电子科技大学计算理论与技术研究所,西安710071

出　　处：《西安交通大学学报》2010年第3期52-57,共6页Journal of Xi'an Jiaotong University

基　　金：国家自然科学基金资助重大国际合作项目(60910004);国家"973计划"重点资助项目(2010CB328102);国家自然科学基金重点资助项目(60433010);国家自然科学基金资助项目(60873018);总装备部预研项目(51315050105)

摘　　要：针对软件测试无法满足多内核处理器上进程调度的验证需要这一问题,提出利用投影时序逻辑(PTL)的定理证明方法来验证进程调度.使用PTL公式建立了支持当前主流进程调度算法的多内核处理器进程调度一般模型S,并将系统期望的性质描述为PTL公式P,在PTL公理系统的基础上,通过证明S蕴含P是否为一个定理来验证系统是否具备该性质.以2内核处理器上的多级反馈队列算法的正确性为案例进行检验,结果表明所提方法可验证多内核处理器进程调度的系统性质,保证多内核进程调度的可靠性.由于多内核处理器的进程调度具备了并发系统的主要特点,因此该方法也适用于一般的并发系统验证.Software testing is unable to meet the verification needs of process scheduling for multi-core CPU,therefore a theorem proving approach with projection temporal logic（PTL） is adapted to verify the process scheduler.A general model supporting the most commonly used scheduling algorithms for multi-core CPU is constructed by a PTL formula S,and the desired property of the system is described by a PTL formula P,then whether the system possesses the property can be identified by proving whether or not S implying P is a theorem based on the axiomatization of PTL.As a case study,the correctness of the processes scheduling with the multilevel feedback queue scheduling algorithm over a two-core CPU is proved,which indicates that the proposed approach can be used to verify system properties of process scheduling over multi-core CPU and hence to ensure the reliability of the process scheduler.Since the process scheduler over multi-core CPU has the typical features of concurrent system,the method can also be applied to verify general concurrent systems.

关 键 词：投影时序逻辑 进程调度 定理证明 多核处理器 调度验证 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]