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

舒新峰; 段振华

您当前的位置：

首页 >

文章列表页 >

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

更新时间：2025-05-01

- 利用投影时序逻辑的多内核进程调度建模与验证
- Modeling and Verification of Processes Scheduling Based on Projection Temporal Logic for Multi-Core CPU
- 西安交通大学学报 2010年44卷第3期页码：52-57
- 作者机构：
  
  西安电子科技大学计算理论与技术研究所,西安,710071
- 作者简介：
- 基金信息：
  
  : 2009-09-28. 作者简介: 舒新峰(1975-),男,博士生;段振华(联系人),男,教授,博士生导师. 基金项目: 国家自然科学基金资助重大国际合作项目(60910004);国家“973计划”重点资助项目(2010CB328102);国家自然科学基金重点资助项目(60433010);国家自然科学基金资助项目(60873018);总装备部预研项目(51315050105)
- DOI：
  中图分类号： TP301
- 网络首发：2010-03-10，
  
  纸质出版：2010
- 稿件说明：
移动端阅览
舒新峰, 段振华. 利用投影时序逻辑的多内核进程调度建模与验证[J]. 西安交通大学学报, 2010,44(3):52-57.

Modeling and Verification of Processes Scheduling Based on Projection Temporal Logic for Multi-Core CPU[J]. 2010, 44(3): 52-57.
舒新峰, 段振华. 利用投影时序逻辑的多内核进程调度建模与验证[J]. 西安交通大学学报, 2010,44(3):52-57. DOI：

Modeling and Verification of Processes Scheduling Based on Projection Temporal Logic for Multi-Core CPU[J]. 2010, 44(3): 52-57. DOI：

摘要

针对软件测试无法满足多内核处理器上进程调度的验证需要这一问题

提出利用投影时序逻辑(PTL)的定理证明方法来验证进程调度.使用PTL公式建立了支持当前主流进程调度算法的多内核处理器进程调度一般模型S

并将系统期望的性质描述为PTL公式P

在PTL公理系统的基础上

通过证明S蕴含P是否为一个定理来验证系统是否具备该性质.以2内核处理器上的多级反馈队列算法的正确性为案例进行检验

结果表明所提方法可验证多内核处理器进程调度的系统性质

保证多内核进程调度的可靠性.由于多内核处理器的进程调度具备了并发系统的主要特点

因此该方法也适用于一般的并发系统验证.

Abstract

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.

关键词

Keywords

references

DUAN Zhenhua. Temporal logic and temporal logic programming [M]. Beijing: Science Press, 2006:35-105.

MOSZKOWSKI B. Executing temporal logic programs [D]. Cambridge, UK: Cambridge University Press, 1986.

TIAN Cong, DUAN Zhenhua. Complexity of propositional projection temporal logic with star [J]. Mathematical Structures in Computer Science, 2009, 19(1): 73-100.

DUAN Zhenhua, ZHANG Nan. A complete axiomatization of propositional projection temporal logic [C]∥Proceedings of 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering. Los Alamitos, CA, USA: IEEE Computer Society, 2008: 271-278.

雷丽晖, 段振华. 基于扩展投影时序逻辑的组合Web 服务描述与验证[J].西安交通大学学报, 2007, 41(10): 1155-1159.

LEI Lihui, DUAN Zhenhua. Specification and verification of composite Web services based on extended projection temporal logic [J]. Journal of Xi'an Jiaotong University, 2007, 41(10): 1155-1159.

雷丽晖, 段振华. 使用扩展区间时序逻辑为并发工作流建模[J]. 西安电子科技大学学报, 2007, 34(4): 673-680.

LEI Lihui, DUAN Zhenhua. Modelling concurrent workflow with the extended interval temporal logic [J]. Journal of Xidian University, 2007, 34(4): 673-680.

王小兵, 段振华. 面向投影时序逻辑的Web服务模型检测[J]. 西安交通大学学报, 2009, 43(4): 41-43.

WANG Xiaobing, DUAN Zhenhua. Projection temporal logic oriented model checking for Web services [J]. Journal of Xi'an Jiaotong University, 2009, 43(4): 41-43.

张海宾,段振华. 混合投影时序逻辑与混合系统的形式化验证[J]. 计算机科学, 2007, 34(11): 279-282.

ZHANG Haibin, DUAN Zhenhua. Hybrid projection temporal logic and formal verifications of hybrid systems [J]. Computer Science, 2007, 34(11): 279-282.

DUAN Zhenhua, YANG X, KOUTNY M. Framed temporal logic programming [J]. Science of Computer Programming, 2008, 70(1): 31-61.

DUAN Zhenhua, TIAN Cong. A unified model checking approach with projection temporal logic [C]∥LNCS 5256: Proceedings of 10th International Conference on Formal Engineering Methods. Berlin, Germany: Springer, 2008: 167-186.

舒新峰, 段振华. 投影时序逻辑的公理系统与形式验证[J].西安电子科技大学学报, 2009, 36(4): 680-685.

SHU Xinfeng, DUAN Zhenhua. Axiomatization for the first-order projection temporal logic and formal verifications [J]. Journal of Xidian University, 2009, 36(4): 680-685.

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于扩展投影时序逻辑的组合Web服务描述与验证

面向投影时序逻辑的Web服务模型检测

面向高海拔空冷发电机防晕性能演化规律的电热耦合研究

结构-语义-残差协同的图像压缩框架：面向隐私保护与高保真重建

电子级超纯氮深冷空分流程节能优化研究