| Verification of Concurrent Assembly Programs with a Petri Net Based Safety Policy |
| |
| 作者姓名： | 王生原 梁英毅 董渊 |
| |
| 作者单位： | Department of Computer Science and Technology Tsinghua University，Department of Computer Science and Technology Tsinghua University，Department of Computer Science and Technology Tsinghua University，Beijing 100084 China，Beijing 100084 China，Beijing 100084 China |
| |
| 基金项目： | 清华大学智能技术与系统国家重点实验室开放性基金;国家自然科学基金;国家高技术研究发展计划(863计划) |
| |
| 摘 要： | Concurrent programs written in a machine level language are being used in many areas but verifi- cation of such programs brings new challenges to the programming language community. Most of the stud- ies in the literature on verifying the safety properties of concurrent programs are for high-level languages, specifications, or calculi. Therefore, more studies are needed on concurrency verification for machine level language programs. This paper describes a framework of a Petri net based safety policy for the verification of concurrent assembly programs, to exploit the capability of Petri nets in concurrency modeling. The con- currency safety properties can be considered separately using the net structure and by mixing Hoare logic and computational tree logic. Therefore, more useful higher-level safety properties can be specified and verified.
|
| 关 键 词： | 程序设计 安全政策 网络 通道水平 |
| 收稿时间： | 2007-01-22 |
| 修稿时间： | 2007-06-30 |
Verification of Concurrent Assembly Programs with a Petri Net Based Safety Policy |
| |
| Shengyuan Wang, , Yingyi Liang, &#x;¼,Yuan Dong, &#x; ê.Verification of Concurrent Assembly Programs with a Petri Net Based Safety Policy[J].Tsinghua Science and Technology,2007,12(6):684-690. |
| |
| Authors: | Shengyuan Wang Yingyi Liang &#x;¼ Yuan Dong &#x; ê |
| |
| Institution: | aDepartment of Computer Science and Technology, Tsinghua University, Beijing 100084, China |
| |
| Abstract: | Concurrent programs written in a machine level language are being used in many areas but verifi- cation of such programs brings new challenges to the programming language community. Most of the stud- ies in the literature on verifying the safety properties of concurrent programs are for high-level languages, specifications, or calculi. Therefore, more studies are needed on concurrency verification for machine level language programs. This paper describes a framework of a Petri net based safety policy for the verification of concurrent assembly programs, to exploit the capability of Petri nets in concurrency modeling. The con- currency safety properties can be considered separately using the net structure and by mixing Hoare logic and computational tree logic. Therefore, more useful higher-level safety properties can be specified and verified. |
| |
| Keywords: | verification machine level concurrent programming Petri nets safety policy verifying/certifying compilers |
| 本文献已被 CNKI 维普 万方数据 ScienceDirect 等数据库收录！ |
