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

您当前的位置：

首页 >

文章列表页 >

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

更新时间：2025-05-01

- Modeling and Verification of Processes Scheduling Based on Projection Temporal Logic for Multi-Core CPU
- Vol. 44, Issue 3, Pages: 52-57(2010)
- 作者机构：
  
  西安电子科技大学计算理论与技术研究所,西安,710071
- 作者简介：
- 基金信息：
- DOI：
  CLC： TP301
- Online First：10 March 2010，
  
  Published：2010
- 稿件说明：
移动端阅览
Modeling and Verification of Processes Scheduling Based on Projection Temporal Logic for Multi-Core CPU[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.

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Specification and Verification of Composite Web Services Based on Extended Projection Temporal Logic

Projection Temporal Logic Oriented Model Checking for Web Services

Knowledge Graph Representation Learning Driven by Semantic Discrimination and Subgraph Integration

I/O Performance Modeling and Prediction Method for Large-Scale Parallel Applications Using Machine Learning

Research on the Electrohydrodynamic Effects of Ionic Liquid-Modified Fuels

Related Author

雷丽晖

段振华

王小兵

Related Institution

No data

⁰