MSVL语言的公理系统的程序验证

doi:10.3969/j.issn.1001-2400.2010.01.017

Abstract

Abstract:

The language MSVL is an interval temporal logic programming language. It can be used for the purpose of modeling, simulation and verification of programs. To prove the correctness of interval temporal logic programs, we present a proof system for MSVL. To do so, a set of state axioms and state inference rules is given to deduce a program into its normal form. In addition, a set of axioms and inference rules over intervals is formalized to transform a program from one state to another. Finally, an example is given to illustrate how the axiom system works.

Key words: verification, temporal logic, normal form, safety, axiom system

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.

References

［1］Manna Z, Pnueli A. Temporal Logic of Reactive and Concurrent Systems［M］. Berlin/Heidelberg: Springer-Verlag, 1992.
［2］Barringer H, Fisher M, Gabbay D, et al. METATEM: a Framework for Programming in Temporal Logic［C］//Proceeding REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formulisms, Correctness, Mook, LNCS 430. Netherlands: Springer, 1989: 94-129.
［3］Fujita M, Kono S, Tanaka H, et al. Tokio: Logic Programming Language Based on Temporal Logic and Its Compilation to PROLOG［C］//Third International Conference on Logic Programming, LNCS 225. London: Springer, 1986: 695-709.
［4］Lamport L. The Temporal Logic of Actions［J］. ACM Transactions on Programming Languages and Systems, 1994(16): 872-923.
［5］Moszkowski B. Executing Temporal Logic Programs［D］. Cambridge: Cambridge University Press, 1986.
［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］Duan Z, Yang X, Koutny M. Framed Temporal Logic Programming ［J］. Science of Computer Programming, 2008, 70(1): 31-61.
［8］雷丽晖, 段振华. 使用扩展区间时序逻辑为并发工作流建模［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.
［9］Yang Xiaoxiao, Duan Zhenhua. Operational Semantics of Framed Temporal Logic Programming Languages［J］. Journal of Logic and Algebraic Programming, 2008, 78(1): 22-51.
［10］Duan Z. An Extended Interval Temporal Logic and A Framing Technique for Temporal Logic Programming ［D］. Glasgow: University of Newcastle Upon Tyne, 1996.
［11］Duan Z. Temporal Logic and Temporal Logic Programming ［M］. Beijing: Science Press, 2006.
［12］Hoare C A R. An Axiomatic Basis for Computer Programming［J］. Communications of ACM, 1969, 12(10): 576-583.

[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]	WANG Yanfen,ZHU Xuran,YUN Xiao,SUN Yanjing,SHI Yunkai,WANG Sainan. Vehicle re-identification by multi-cameras for public security surveillance [J]. Journal of Xidian University, 2019, 46(4): 190-196.
[5]	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.
[6]	DUAN Zhao, LIU Kunlong. Dynamic program verification via a CPAChecker [J]. Journal of Xidian University, 2019, 46(1): 33-38.
[7]	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.
[8]	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.
[9]	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.
[10]	FAN Quanrun;DUAN Zhenhua. Two phase clustering method for CNF clauses [J]. Journal of Xidian University, 2016, 43(3): 55-60.
[11]	MA Qian;DUAN Zhenhua. Automatic theorem proving technique for MSVL [J]. J4, 2016, 43(1): 75-81.
[12]	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.
[13]	ZHANG Nan;DUAN Zhenhua. Compositional verification of a carry-save adder with the propositional projection temporal logic [J]. J4, 2012, 39(5): 192-196.
[14]	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.
[15]	WANG Shiqiang;ZHANG Dengfu;BI Duyan;YONG Xiaoju. Novel radar signal sorting method with low complexity [J]. J4, 2011, 38(4): 148-153.

Verification of programs based on an axiom system for the MSVL language

PDF (PC)

Like

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Metrics

Comments

Recommended 10