一种命题投影时序逻辑的分布式模型检测方法

doi:10.19665/j.issn1001-2400.2020.04.006

摘要/Abstract

摘要：

为缓解模型检测的状态空间爆炸问题,提出一种基于命题投影时序逻辑的分布式模型检测方法。通过标记范式图技术将命题投影时序逻辑公式描述的待验证性质转换为自动机;根据强连通分量将其状态空间划分为多个子自动机,将各个子自动机与层次语法图描述的待验证系统模型分发至验证服务器集群中,使用动态验证技术进行多机协同完成系统模型检测验证。实验结果表明,该方法和单机模型检测相比验证时间明显降低,且能够验证更复杂的系统。

关键词: 命题投影时序逻辑, 模型检测, 形式化验证, 标记范式图, 分布式计算

Abstract:

To alleviate the state-explosion problem of model checking, a novel distributed model checking method based on the propositional projection temporal logic (PPTL). First, the property to be verified in the PPTL formula is transformed into an automaton with the technique of Labeled Normal Form Graph, which in turn is partitioned into multiple subautomata according to the strongly connected components. Then, each subautomaton and the system model in the Hierarchical Syntax Chart are delivered to the members of the verification server cluster, and model checking of the system is implemented in parallel with the on-the-fly technique on multiple computers. Experimental results indicate that, compared with the standalone model checking approach, the proposed method can not only significantly reduce the time consumption but also verify more complex systems.

Key words: propositional projection temporal logic, model checking, formal verification, labeled normal form graph, distributed computing

中图分类号:

TP302.7

舒新峰,王昌太,王燕,张丽丽. 一种命题投影时序逻辑的分布式模型检测方法[J]. 西安电子科技大学学报, 2020, 47(4): 39-47.

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.

图/表 5

参考文献 19

[1]	CLARKE E M, HENZINGER T A, VEITH H, et al. Handbook of Model Checking//Introduction to Model Checking[M]. Heidelberg: Springer International Publishing, 2018: 1-26.
[2]	段钊, 刘锟龙. 采用CPAChecker的动态程序验证[J]. 西安电子科技大学学报, 2019,46(1):33-38.
	DUAN Zhao, LIU Kunlong. Dynamic Program Verification via a CPAChecker[J]. Journal of Xidian University, 2019,46(1):33-38.
[3]	BAIER C, HAVERKORT B, HERMANNS H, et al. Model Checking Continuous-time Markov Chains by Transient Analysis[C]// Lecture Notes in Computer Science: 1855. Heidelberg: Springer Verlag, 2000: 358-372.
[4]	ZHANG G Q, RONG M. An Approach of Concurrent Object-Oriented Program Slicing Based on LTL Property[C]// Proceedings of the 2008 International Conference on Computer Science and Software Engineering. Washington: IEEE Computer Society, 2008: 650-653.
[5]	MATEESCU R, REQUENO J I. On-the-fly Model Checking for Extended Action-based Probabilistic Operators[C]// Lecture Notes in Computer Science: 9641. Heidelberg: Springer Verlag, 2016: 189-207.
[6]	BARNAT J, BRIM L, ROCKAI P. Scalable Multi-core LTL Model-checking[C]// Lecture Notes in Computer Science: 4595. Heidelberg: Springer Verlag, 2007: 187-203.
[7]	BRIM L, CERNA I, KRCAL P, et al. Distributed LTL Model Checking Based on Negative Cycle Detection[C]// Lecture Notes in Computer Science: 2245. Heidelberg: Springer Verlag, 2001: 96-107.
[8]	BURNS E, ZHOU R. Parallel Model Checking Using Abstraction[C]// Lecture Notes in Computer Science: 7385. Heidelberg: Springer Verlag, 2012: 172-190.
[9]	DUAN Z H, TIAN C, ZHANG N, et al. Index Set Expressions Can Represent Temporal Logic Formulas[J]. Theoretical Computer Science, 2019,788:21-38. doi: 10.1016/j.tcs.2018.11.030
[10]	KLAUDEL H, KOUTNY M, DUAN Z H, et al. From Box Algebra to Interval Temporal Logic[J]. Fundamenta Informaticae, 2019,167(4):323-354. doi: 10.3233/FI-2019-1820
[11]	DUAN Z H, TIAN C, ZHANG N. A Canonical Form Based Decision Procedure and Model Checking Approach for Propositional Projection Temporal Logic[J]. Theoretical Computer Science, 2016,609:544-560. doi: 10.1016/j.tcs.2015.08.039
[12]	SHU X F, ZHANG N. An Efficient Decision Procedure for Propositional Projection Temporal Logic[C]// Lecture Notes in Computer Science: 11653. Heidelberg: Springer Verlag, 2019: 503-515.
[13]	WANG M, TIAN C, ZHANG N, et al. Verifying Full Regular Temporal Properties of Programs via Dynamic Program Execution[J]. IEEE Transactions on Reliability, 2019,68(3):1101-1116. doi: 10.1109/TR.24
[14]	马倩, 段振华. MSVL程序的自动定理证明方法[J]. 西安电子科技大学学报, 2016,43(1):75-81. doi: 10.3969/j.issn.1001-2400.2016.01.014
	MA Qian, DUAN Zhenhua. AutomaticTheorem Proving Technique for MSVL[J]. Journal of Xidian University, 2016,43(1):75-81. doi: 10.3969/j.issn.1001-2400.2016.01.014
[15]	TIAN C, DUAN Z H. Expressiveness of Propositional Projection Temporal Logic with Star[J]. Theoretical Computer Science, 2011,412(18):1729-1744. doi: 10.1016/j.tcs.2010.12.047
[16]	CUI J, DUAN Z H, TIAN C, et al. A Novel Approach to Modeling and Verifying Real-Time Systems for High Reliability[J]. IEEE Transactions on Reliability, 2018,67(2):481-493. doi: 10.1109/TR.24
[17]	逢涛, 段振华, 刘晓芳. Verilog程序的命题投影时序逻辑符号模型检测[J]. 西安电子科技大学学报, 2014,41(2):79-84. doi: 10.3969/j.issn.1001-2400.2014.02.013
	PANG Tao, DUAN Zhenhua, LIU Xiaofang. SymbolicModel Checking of Verilog Programs with the Propositional Projection Temporal Logic[J]. Journal of Xidian University, 2014,41(2):79-84. doi: 10.3969/j.issn.1001-2400.2014.02.013
[18]	杨琛, 段振华. PPTL模型检测器实现的一个关键技术[J]. 西安交通大学学报, 2010,44(10):29-34.
	YANG Chen, DUAN Zhenhua. A Key Technique to Develop the Model Checker for Propositional Projection Temporal Logic[J]. Journal of Xi’an Jiaotong University, 2010,44(10):29-34.
[19]	SHU X F, LI C, LIU C. A Visual Modeling Language for MSVL[C]// Lecture Notes in Computer Science: 10189. Heidelberg: Springer Verlag, 2016: 220-237.