投影时序逻辑的公理系统与形式验证

J4 ›› 2009, Vol. 36 ›› Issue (4): 680-729.

投影时序逻辑的公理系统与形式验证

舒新峰^1,2,段振华¹

(1. 西安电子科技大学计算理论与技术研究所，陕西西安 710071；
2. 西安邮电学院计算机系，陕西西安 710121)

收稿日期:2009-01-19 出版日期:2009-08-20 发布日期:2009-09-28
通讯作者: 舒新峰
基金资助:
国家自然科学基金资助(60873018);国家自然科学基金重点项目资助(60433010)

Axiomatization for the first-order projection temporal logic and formal verifications

SHU Xin-feng^1,2;DUAN Zhen-hua¹

(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)

Received:2009-01-19 Online:2009-08-20 Published:2009-09-28
Contact: SHU Xin-feng

摘要/Abstract

摘要：

为了采用定理证明的方法对并发及交互式系统进行验证，提出了一阶投影时序逻辑的公理系统．利用投影时序逻辑既可描述待验证系统性质和规范，又可描述其实现模型的特点，在同一投影时序逻辑框架可以方便地对待验证系统进行建模和性质描述，并使用公理系统完成系统性质的证明．最后通过一个实例来展示投影时序逻辑及公理系统在系统验证中的应用．

关键词: 投影时序逻辑, 公理系统, 形式化方法, 验证

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.

Key words: projection temporal logic, axiomatization, formal methods, verification

中图分类号:

TP301

舒新峰;段振华. 投影时序逻辑的公理系统与形式验证[J]. J4, 2009, 36(4): 680-729.

SHU Xin-feng;DUAN Zhen-hua. Axiomatization for the first-order projection temporal logic and formal verifications[J]. J4, 2009, 36(4): 680-729.

参考文献

［1］Manna Z, Pnueli A. Temporal Logic of Reactive and Concurrent Systems［M］. Berlin: Springer-Verlag, 1992.
［2］Clarke E, Emerson E, Sistla A. Automatic Verification of Finite State Concurrent System Using Temporal Logical Specification［J］. ACM Trans on Programming Language and Systems, 1986, 8(2): 244-263
［3］Moszkowski B. Executing Temporal Logic Programs［D］. Cambridge: Cambridge University, 1986.
［4］Duan Z, Yang X, Koutny M. Framed Temporal Logic Programming［J］. Science of Computer Programming, 2008, 70(1): 31-61.
［5］Duan Z. Temporal Logic and Temporal Logic Programming ［M］. Beijing: Science Press, 2006.
［6］Duan Z, Tian C. A Unified Model Checking Approach with Projection Temporal Logic［C］//10th International Conference on Formal Engineering Methods, LNCS 5256. Berlin: Springer, 2008: 167-186.
［7］雷丽晖, 段振华. 使用扩展区间时序逻辑为并发工作流建模［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.
［8］雷丽晖, 段振华. 基于扩展投影时序逻辑的组合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.
［9］张海宾, 段振华. 稠密时间区间时序逻辑的可满足性判定［J］. 西安电子科技大学学报, 2007, 34(3): 463-467
Zhang Haibin, Duan Zhenhua. Decidability of the Dense Timed Interval Temporal Logic ［J］. Journal of Xidian University, 2007, 34(3): 463-467
［10］王小兵, 段振华. 框架投影时序逻辑程序设计语言中的指针［J］. 西安电子科技大学学报, 2008, 35(6): 1069-1074.
Wang Xiaobing, Duan Zhenhua. Pointers in Framing Projection Temporal Logic Programming Languages ［J］. Journal of Xidian University, 2008, 35(6): 1069-1074.
［11］Duan Z, Tian C, Zhang L. A Decision Procedure for Propositional Projection Temporal Logic with Infinite Models［J］. Acta Information, 2008, 45(1): 43-78.

[1]	沈利香,慕德俊,曹国,谢光前,束方勇. 针对硬件木马的形式化验证模型构造方法[J]. 西安电子科技大学学报, 2021, 48(3): 146-153.
[2]	杨颜博,张嘉伟,马建峰. 一种使用区块链保护车联网数据隐私的方法[J]. 西安电子科技大学学报, 2021, 48(3): 21-30.
[3]	陈思吉,翟社平,汪一景. 一种基于环签名的区块链隐私保护算法[J]. 西安电子科技大学学报, 2020, 47(5): 86-93.
[4]	舒新峰,王昌太,王燕,张丽丽. 一种命题投影时序逻辑的分布式模型检测方法[J]. 西安电子科技大学学报, 2020, 47(4): 39-47.
[5]	于金霞,何旭,闫玺玺. 机构可验证的密文策略属性基加密方案[J]. 西安电子科技大学学报, 2019, 46(4): 49-57.
[6]	陈矗. RFCcertDT:SSL/TLS中证书验证的测试工具[J]. 西安电子科技大学学报, 2019, 46(3): 20-25.
[7]	丁明,张书玲,张琛,张军. 一种航空电子系统安全性需求验证方法[J]. 西安电子科技大学学报, 2019, 46(3): 66-73.
[8]	段钊, 刘锟龙. 采用CPAChecker的动态程序验证[J]. 西安电子科技大学学报, 2019, 46(1): 33-38.
[9]	秦茂源;慕德俊;胡伟;毛保磊. 硬件安全门级细粒度形式化验证方法[J]. 西安电子科技大学学报, 2018, 45(5): 143-148.
[10]	曹鹏;保宏;杜敬利;彭福军. 空间薄膜天线索膜结构建模与形状优化[J]. 西安电子科技大学学报, 2018, 45(2): 54-58+65.
[11]	应作斌;马建峰;崔江涛. 支持位置验证和策略变更的属性加密方案[J]. 西安电子科技大学学报, 2017, 44(2): 57-62+190.
[12]	苗银宾;马建峰;刘志全;魏福山;王绪安. 关键字域可变的可验证密文检索[J]. 西安电子科技大学学报, 2017, 44(1): 52-58.
[13]	黄春水;任艳丽;蔡建兴. 可验证模指数批计算外包方案[J]. 西安电子科技大学学报, 2016, 43(4): 135-140.
[14]	马倩;段振华. MSVL程序的自动定理证明方法[J]. J4, 2016, 43(1): 75-81.
[15]	逄涛;段振华;刘晓芳. Verilog程序的命题投影时序逻辑符号模型检测[J]. J4, 2014, 41(2): 79-84.