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

doi:10.3969/j.issn.1001-2400.2011.02.027

J4 ›› 2011, Vol. 38 ›› Issue (2): 151-156.doi: 10.3969/j.issn.1001-2400.2011.02.027

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

杨琛^1,2,3;段振华^1,2

(1. 西安电子科技大学计算理论与技术研究所，陕西西安 710071;
2. 西安电子科技大学综合业务网理论及关键技术国家重点实验室，陕西西安 710071;
3. 武汉大学软件工程国家重点实验室，湖北武汉 430072)

收稿日期:2010-02-10 出版日期:2011-04-20 发布日期:2011-05-26
作者简介:杨琛(1981-)，男，西安电子科技大学博士研究生，E-mail: chyang@mail.xidian.edu.cn．
基金资助:
国家自然科学基金重大国际合作项目资助项目(60910004);国家自然科学基金资助项目(60433010,60873018);国家重点基础研究发展计划(973)资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项基金资助项目(JY10000903004)

Stutter-invariant propositional interval temporal logic

YANG Chen^1,2,3;DUAN Zhenhua^1,2

(1. Research Inst. of Computing Theory & Technology, Xidian Univ., Xi'an 710071， China;
2. State Key Lab. of Integrated Service Networks, Xidian Univ., Xi'an 710071， China;
3. State Key Lab. of Software Eng., Wuhan Univ., Wuhan 430072， China)

Received:2010-02-10 Online:2011-04-20 Published:2011-05-26

摘要/Abstract

摘要：

为了将命题区间时序逻辑(PITL)应用于组合验证，并降低组合产生的状态爆炸风险，提出了支持Stutter-不变性的命题区间时序逻辑PITLst．PITLst继承了PITL的结构相关性，可表达所有PITL能够表达的Stutter-不变性质，支持模块抽象约简系统规模，降低了状态爆炸风险．自动加油站模型的组合验证实例表明，PITLst可有效应用于组合验证技术．

关键词: 模型检测, 时序逻辑, 状态爆炸

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

杨琛;段振华. 支持Stutter-不变性的命题区间时序逻辑[J]. J4, 2011, 38(2): 151-156.

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

参考文献

［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]	沈利香,慕德俊,曹国,谢光前,束方勇. 针对硬件木马的形式化验证模型构造方法[J]. 西安电子科技大学学报, 2021, 48(3): 146-153.
[2]	舒新峰,王昌太,王燕,张丽丽. 一种命题投影时序逻辑的分布式模型检测方法[J]. 西安电子科技大学学报, 2020, 47(4): 39-47.
[3]	丁明,张书玲,张琛,张军. 一种航空电子系统安全性需求验证方法[J]. 西安电子科技大学学报, 2019, 46(3): 66-73.
[4]	段钊, 刘锟龙. 采用CPAChecker的动态程序验证[J]. 西安电子科技大学学报, 2019, 46(1): 33-38.
[5]	马倩;段振华. MSVL程序的自动定理证明方法[J]. J4, 2016, 43(1): 75-81.
[6]	逄涛;段振华;刘晓芳. Verilog程序的命题投影时序逻辑符号模型检测[J]. J4, 2014, 41(2): 79-84.
[7]	张南;段振华. 进位保留加法器的命题投影时序逻辑组合验证[J]. J4, 2012, 39(5): 192-196.
[8]	杨元原;马文平;刘维博;俞优;顾健. 带有异或运算安全协议的自动化检测[J]. J4, 2012, 39(4): 120-125+183.
[9]	王小兵;段振华. 框架时序逻辑语言MSVL中面向对象机制的实现[J]. J4, 2010, 37(3): 559-564+575.
[10]	杨潇潇;段振华. MSVL语言的公理系统的程序验证[J]. J4, 2010, 37(1): 96-101.
[11]	舒新峰;段振华. 投影时序逻辑的公理系统与形式验证[J]. J4, 2009, 36(4): 680-729.
[12]	张海宾;段振华. 区间时序逻辑的模型检查 [J]. J4, 2009, 36(2): 338-342.
[13]	王小兵;段振华. 框架投影时序逻辑程序设计语言中的指针 [J]. J4, 2008, 35(6): 1069-1074.
[14]	张海宾;段振华. 多速率混合系统的模型检查 [J]. J4, 2008, 35(1): 60-648.
[15]	雷丽晖;段振华. 使用扩展区间时序逻辑为并发工作流建模 [J]. J4, 2007, 34(4): 673-680.

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

Stutter-invariant propositional interval temporal logic

PDF (PC)

赞

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

Metrics

本文评价

推荐阅读 0