| 投影时序逻辑的公理系统与形式验证 |
| |
| 引用本文： | 舒新峰,段振华.投影时序逻辑的公理系统与形式验证[J].西安电子科技大学学报,2009,36(4):680-729. |
| |
| 作者姓名： | 舒新峰 段振华 |
| |
| 作者单位： | (1. 西安电子科技大学 计算理论与技术研究所，陕西 西安710071；2. 西安邮电学院 计算机系，陕西 西安710121) |
| |
| 基金项目： | 国家自然科学基金资助，国家自然科学基金重点项目资助 |
| |
| 摘 要： | 为了采用定理证明的方法对并发及交互式系统进行验证，提出了一阶投影时序逻辑的公理系统．利用投影时序逻辑既可描述待验证系统性质和规范，又可描述其实现模型的特点，在同一投影时序逻辑框架可以方便地对待验证系统进行建模和性质描述，并使用公理系统完成系统性质的证明．最后通过一个实例来展示投影时序逻辑及公理系统在系统验证中的应用．
|
| 关 键 词： | 投影时序逻辑 公理系统 形式化方法 验证 |
| 收稿时间： | 2009-01-19 |
Axiomatization for the first-order projection temporal logic and formal verifications |
| |
| SHU Xin-feng,DUAN Zhen-hua.Axiomatization for the first-order projection temporal logic and formal verifications[J].Journal of Xidian University,2009,36(4):680-729. |
| |
| Authors: | SHU Xin-feng DUAN Zhen-hua |
| |
| Affiliation: | (1. Research Inst. of Computing Theory & Technology, Xidian Univ., Xi'an 710071， China;
2. Dept. of Computer Sci., Xi'an Inst. of Posts and Telecommunications, Xi'an 710121， China) |
| |
| Abstract: | To verify the properties of the concurrent and reactive systems based on the theorem proving approach, an axiomatization is formulized for the first order projection temporal logic (FPTL). Further, FPTL can be used to describe the properties as well as the implementation of the system to be verified, which enables us to do verification within the same logic framework. Finally, an example is given to illustrate how to do system verification based on FPTL and its axiomatic system. |
| |
| Keywords: | projection temporal logic axiomatization formal methods verification |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《西安电子科技大学学报》浏览原始摘要信息 |
|
点击此处可从《西安电子科技大学学报》下载全文 |
