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

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

CLC Number:

TP301

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

References

［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]	SHEN Lixiang,MU Dejun,CAO Guo,XIE Guangqian,SHU Fangyong. Constructing formal verification models for hardware Trojans [J]. Journal of Xidian University, 2021, 48(3): 146-153.
[2]	CHEN Siji,ZHAI Sheping,WANG Yijing. Blockchain privacy protection algorithm based on ring signature [J]. Journal of Xidian University, 2020, 47(5): 86-93.
[3]	SHU Xinfeng,WANG Changtai,WANG Yan,ZHANG Lili. Propositional projection temporal logic based distributed model checking method [J]. Journal of Xidian University, 2020, 47(4): 39-47.
[4]	DING Ming,ZHANG Shuling,ZHANG Chen,Zhang Jun. Method for the verification of safety requirements of avionics systems [J]. Journal of Xidian University, 2019, 46(3): 66-73.
[5]	DUAN Zhao, LIU Kunlong. Dynamic program verification via a CPAChecker [J]. Journal of Xidian University, 2019, 46(1): 33-38.
[6]	QIN Maoyuan;MU Dejun;HU Wei;MAO Baolei. Fine-granularity gate level formal verification method for hardware security [J]. Journal of Xidian University, 2018, 45(5): 143-148.
[7]	CAO Peng;BAO Hong;DU Jingli;PENG Fujun. Cable-membrane modeling and shape optimization of the space membrane antenna [J]. Journal of Xidian University, 2018, 45(2): 54-58+65.
[8]	YING Zuobin;MA Jianfeng;CUI Jiangtao. Attribute-based encryption with location verification and policy adjusting supporting the cloud mobile office [J]. Journal of Xidian University, 2017, 44(2): 57-62+190.
[9]	MA Qian;DUAN Zhenhua. Automatic theorem proving technique for MSVL [J]. J4, 2016, 43(1): 75-81.
[10]	PANG Tao;DUAN Zhenhua;LIU Xiaofang. Symbolic model checking of Verilog programs with the propositional projection temporal logic [J]. J4, 2014, 41(2): 79-84.
[11]	ZHANG Nan;DUAN Zhenhua. Compositional verification of a carry-save adder with the propositional projection temporal logic [J]. J4, 2012, 39(5): 192-196.
[12]	ZHANG Ximin;WEI Ting. Research on the test and verification system of the ARINC 659 fault-tolerant backplane data bus [J]. J4, 2011, 38(6): 140-145.
[13]	WANG Shiqiang;ZHANG Dengfu;BI Duyan;YONG Xiaoju. Novel radar signal sorting method with low complexity [J]. J4, 2011, 38(4): 148-153.
[14]	YANG Xiao-xiao;DUAN Zhen-hua. Verification of programs based on an axiom system for the MSVL language [J]. J4, 2010, 37(1): 96-101.
[15]	JIA Xiao-yun1;3;LUO Shou-shan2;3;YUAN Chao-wei1. New digital signature scheme based on the discrete logarithm [J]. J4, 2008, 35(2): 351-355.

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

PDF (PC)

Like

Knowledge

Cited

Abstract

Cite this article

share this article

References

Related Articles 15

Metrics

Comments

Recommended 10