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

发布时间：2021-11-15 02:08

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

【文章来源】：西安电子科技大学学报. 2020,47(04)北大核心EICSCD

【文章页数】：9 页

【部分图文】：

命题投影时序逻辑公式p;q的标记范式图

层次语法图（Hierarchical Syntax Chart,HSC）是文献[19]中用来描述面向过程软件系统执行方案语法结构的工具，可通过软件系统的设计模型或软件系统的源码进行构造。层次语法图将系统的执行模型递归描述为复合语句序列，每个复合语句由复合语句名称和复合语句体构成，复合语句体为语句序列。层次语法图的结构如图2所示。第一层为函数复合语句，复合语句名称（圆形顶点）为函数名，复合语句体为函数体语句（方形顶点）构成的语句序列。特别地，当复合语句体中包含if或while语句时，如函数Fun1中的if语句，其Yes分支和No分支也分别递归描述为复合语句（while语句结构无No分支）。层次语法图的形式化定义如下：

命题投影时序逻辑分布式模型检测采用主从模式的分布式框架，验证过程如图3所示。将待验证系统的层次语法图模型S和命题投影时序逻辑公式描述的待验证系统性质P输入到调度服务器中，对P使用标记范式图技术构造性质非自动机Ap，然后根据强连通分量将其状态空间划分为多个子自动机ai p并送入任务队列中。调度服务器监听各验证服务器的状态。当存在空闲服务器时，在任务队列中取出一个子自动机ai p和层次语法图表达的待检测系统模型S送入该服务器进行模型检测验证，并将验证结果返回到调度服务器中。下面重点给出状态空间划分算法和模型检测算法。2.2 性质非自动机状态空间划分算法

【参考文献】：
期刊论文
[1]采用CPAChecker的动态程序验证[J]. 段钊,刘锟龙.  西安电子科技大学学报. 2019(01)
[2]MSVL程序的自动定理证明方法[J]. 马倩,段振华.  西安电子科技大学学报. 2016(01)
[3]Verilog程序的命题投影时序逻辑符号模型检测[J]. 逄涛,段振华,刘晓芳.  西安电子科技大学学报. 2014(02)
[4]PPTL模型检测器实现的一个关键技术[J]. 杨琛,段振华.  西安交通大学学报. 2010(10)



本文编号：3495814