支持Stutter-不变性的命题区间时序逻辑

doi:10.3969/j.issn.1001-2400.2011.02.027

Abstract

Abstract:

To apply the propositional interval temporal logic (PITL) in compositional verification with minor risk of state-exlopsion, a stutter-invariant PITL (PITLst) is proposed, which is structure-related since it inherits the structural relativity of PITL operators much like constructs of imperative programming, such as chop operator for sequential composition and projection opertor for iteration, thus when used as a specification language PITLst can specify the structure of concurrent systems. Moreover, it is shown that PITLst can express all stutter-invariant properties expressible in PITL, so it surpports modular abstraction for compositional verification. In this way, the overall system is of small size, so the risk of state-explosion is accordingly reduced. In addition, an automatic gas station system, as an example, is compositionally verified against PITLst properties, which illustrates that PITLst well supports compositional verfication.

Key words: model checking, temporal logic, state explosion

YANG Chen;DUAN Zhenhua. Stutter-invariant propositional interval temporal logic[J].J4, 2011, 38(2): 151-156.

References

［1］ Moszkowski B C. Executing Temporal Logic ［D］. Cambridge: Department of Computer Science, Cambridge University, 1986.
［2］ Lichtenstein O, Pnueli A. Checking that Finite State Concurrent Programs Satisfy Their Linear Specification ［C］//Proceedings of the 12th Annual ACM Symposium on Principles of Programming Languages. New York: ACM, 1985: 97-107.
［3］ Clarke E M, Long D, McMillan K. Compositional Model Checking ［C］//Proc LICS'89. New York: IEEE Press, 1986: 353-362.
［4］曾红卫, 缪淮扣. 构件组合的抽象精化验证［J］. 软件学报,2008 19(5): 1149-1159.
Zeng Hongwei, Miao Huaikou. Verification of Component Composition Based on Abstraction Refinement ［J］. Journal of Software, 2008, 19(5): 1149-1159.
［5］ Holzmann GJ. The Spin Model Checker: Primer and Reference Manual ［M］. New York: Addison-Wesley, 2003.
［6］ Valmari A. The State Explosion Problem ［J］. Lecture Notes in Computer Science, Springer-Verlag, 1998(1491): 429-528.
［7］杨琛. 基于进程代数并发系统的建模与验证研究［D］. 西安: 西北大学，2006.
［8］ Peled D, Wilke T. Stutter-Invariant Temporal Properties are Expressible without the Next-Time Operator ［J］. Information Processing Letter, 1997, 63(6):243-246.
［9］张海滨, 段振华. 区间时序逻辑的模型检查［J］. 西安电子科技大学学报, 2009, 36(2): 338-342.
Zhang Haibing, Duan Zhenhua. Model Checking Interval Temporal Logic ［J］. Journal of Xidian University, 2009, 36(2): 338-342.
［10］ Bowman H, Thompson S J. A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection ［J］. Journal of Logic and Computation, 2003, 13(2):195-239.
［11］ Helmbold D, Luckham D. Debugging Ada Tasking Programs ［J］. IEEE Software, 1985, 2(2): 47-57.
［12］ Hoare CAR. Communicating Sequential Processes ［M］. London: Prentice Hall, 1985.

[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]	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.
[3]	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.
[4]	DUAN Zhao, LIU Kunlong. Dynamic program verification via a CPAChecker [J]. Journal of Xidian University, 2019, 46(1): 33-38.
[5]	MA Qian;DUAN Zhenhua. Automatic theorem proving technique for MSVL [J]. J4, 2016, 43(1): 75-81.
[6]	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.
[7]	ZHANG Nan;DUAN Zhenhua. Compositional verification of a carry-save adder with the propositional projection temporal logic [J]. J4, 2012, 39(5): 192-196.
[8]	YANG Yuanyuan;MA Wenping;LIU Weibo;YU You;GU Jian. Automatic detection of security protocols with XOR [J]. J4, 2012, 39(4): 120-125+183.
[9]	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.
[10]	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.
[11]	SHU Xin-feng;DUAN Zhen-hua. Axiomatization for the first-order projection temporal logic and formal verifications [J]. J4, 2009, 36(4): 680-729.
[12]	ZHANG Hai-bin;DUAN Zhen-hua. Model checking interval temporal logic [J]. J4, 2009, 36(2): 338-342.
[13]	WANG Xiao-bing;DUAN Zhen-hua. Pointers in framing projection temporal logic programming languages [J]. J4, 2008, 35(6): 1069-1074.
[14]	ZHANG Hai-bin;DUANG Zhen-hua. Model checking multirate hybrid systems [J]. J4, 2008, 35(1): 60-648.
[15]	GUO Jian1;JIN Nai-yong2. Vacuity detection in computation temperal logic [J]. J4, 2007, 34(5): 794-799.

Stutter-invariant propositional interval temporal logic

PDF (PC)

Like

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Metrics

Comments

Recommended 10