MSVL程序的自动定理证明方法

doi:10.3969/j.issn.1001-2400.2016.01.014

Abstract

Abstract:

The MSVL is a temporal logic programming language. It can be used to verify C, Verilog/VHDL programs. To do so, a program written in C or Verilog/VHDL is translated to an MSVL program, and then the task is changed to verify MSVL programs. However, at present, the correctness of MSVL programs can only be proved by hand with deductive approaches. This is tedious and error-prone. To handle this problem, an automatic theorem proving technique for the MSVL based on the interactive theorem prover PVS is proposed. To this end, first the syntax and semantics of the MSVL are described in the specification language of PVS, which enables MSVL programs to be correctly recognized by PVS. Further, an axiomatic system of the MSVL and some theorems are specified. Then the proof commands of PVS are input for invoking the PVS prover to deduce MSVL programs. During verification, simple details can be proved by PVS automatically while complex steps are controlled by human. In this way, MSVL programs can be verified semi-automatically, which facilitates the deduction of MSVL programs. An instance of the bakery algorithm is given to show that our method is feasible.

Key words: temporal logic, axiomatic system, theorem proving, verification

MA Qian;DUAN Zhenhua. Automatic theorem proving technique for MSVL[J].J4, 2016, 43(1): 75-81.

References

［1］ de BOER F, BONSANGUE M, ROT J. Automated Verification of Recursive Programs with Pointers ［C］//Lecture Notes in Computer Science: 7364 LNAI. Heidelberg: Springer Verlag, 2012: 149-163.
［2］ BERTOT Y, CASTRAN P. Interactive Theorem Proving and Program Development ［M］. Berlin: Springer Verlag, 2004.
［3］ OWRE S, SHANKAR N, RUSHBY J M, et al. PVS Language Reference ［EB/OL］. ［2014-09-10］. http://www.docin.com/p.454926227.html.
［4］ NERON P. Square Root and Division Elimination in PVS ［C］//Lecture Notes in Computer Science: 7998 LNCS. Heidelberg: Springer Verlag, 2013: 457-462.
［5］ DUAN Z. Temporal Logic and Temporal Logic Programming ［M］. Beijing: Science Press of China, 2006.
［6］ TANG C S. A Temporal Logic Language Oriented toward Software Engineering-Introduction to XYZ System (I) ［J］. Chinese Journal of Advanced Software Research, 1994, 1(1): 1-27.
［7］ LAMPORT L. The Temporal Logic of Actions ［J］. ACM Transactions on Programming Language and Systems, 1994, 16(3): 872-923.
［8］ MOSZKOWSKI B. Executing Temporal Logic Programs ［D］. Cambridge: Cambridge University, 1986.
［9］ YANG X, DUAN Z, MA Q. Axiomatic Semantics of Projection Temporal Logic Programs ［J］. Mathematical Structures in Computer Science, 2010, 20(5): 865-914.
［10］张南, 段振华. 进位保留加法器的命题投影时序逻辑组合验证［J］. 西安电子科技大学学报, 2012, 39(5): 192-196.
ZHANG Nan, DUAN Zhenhua. Compositional Verification of a Carry-save Adder with the Propositional Projection Temporal Logic ［J］. Journal of Xidian University, 2012, 39(5): 192-196.
［11］逄涛, 段振华, 刘晓芳. Verilog程序的命题投影时序逻辑符号模型检测［J］. 西安电子科技大学学报, 2014, 41(2): 79-84.
PANG Tao, DUAN Zhenhua, LIU Xiaofang. Symbolic Model Checking of Verilog Programs with The Propositional Projection Temporal Logic ［J］. Journal of Xidian University, 2014, 41(2): 79-84.
［12］ LAMPORT L. A New Solution of Dijkstra's Concurrent Programming Problem ［J］. Communications of the ACM, 1974, 17(8): 453-455.
［13］ DUAN Z H, TIAN C, YANG M F, et al. Bounded Model Checking for Propositional Projection Temporal Logic ［C］//Lecture Notes in Computer Science: 7936 LNCS. Heidelberg: Springer Verlag, 2013: 591-602.

[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]	DUAN Zhao, LIU Kunlong. Dynamic program verification via a CPAChecker [J]. Journal of Xidian University, 2019, 46(1): 33-38.
[5]	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.
[6]	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.
[7]	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.
[8]	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.
[9]	ZHANG Nan;DUAN Zhenhua. Compositional verification of a carry-save adder with the propositional projection temporal logic [J]. J4, 2012, 39(5): 192-196.
[10]	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.
[11]	WANG Shiqiang;ZHANG Dengfu;BI Duyan;YONG Xiaoju. Novel radar signal sorting method with low complexity [J]. J4, 2011, 38(4): 148-153.
[12]	YANG Chen;DUAN Zhenhua. Stutter-invariant propositional interval temporal logic [J]. J4, 2011, 38(2): 151-156.
[13]	WANG Xiao-bing;DUAN Zhen-hua. Implementation of objected-oriented mechanism in framed temporal logic language MSVL [J]. J4, 2010, 37(3): 559-564+575.
[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]	SHU Xin-feng;DUAN Zhen-hua. Axiomatization for the first-order projection temporal logic and formal verifications [J]. J4, 2009, 36(4): 680-729.

Automatic theorem proving technique for MSVL

PDF (PC)

Like

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Metrics

Comments

Recommended 10