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

Propositional projection temporal logic based distributedmodel checking method

作　　者：舒新峰 王昌太 王燕 张丽丽 SHU Xinfeng;WANG Changtai;WANG Yan;ZHANG Lili(School of Computer Science,Xi′an University of Posts and Telecommunications,Xi′an 710121,China)

机构地区：[1]西安邮电大学计算机学院,陕西西安710121

出　　处：《西安电子科技大学学报》2020年第4期39-47,共9页Journal of Xidian University

基　　金：国家自然科学基金(61672403,61972301);陕西省重点研发计划(2020GY-210);咸阳市科学技术研究计划(2017K01-25-8)。

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

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

分 类 号：TP302.7[自动化与计算机技术—计算机系统结构]