一种命题投影时序逻辑的分布式模型检测方法
Propositional projection temporal logic based distributedmodel checking method作者机构：西安邮电大学计算机学院陕西西安710121
出 版 物：《西安电子科技大学学报》 (Journal of Xidian University)
年 卷 期：2020年第47卷第4期
页 面：39-47页
核心收录：
学科分类：0808[工学-电气工程] 0809[工学-电子科学与技术（可授工学、理学学位）] 08[工学] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：国家自然科学基金(61672403,61972301) 陕西省重点研发计划(2020GY-210) 咸阳市科学技术研究计划(2017K01-25-8)。
主 题：命题投影时序逻辑 模型检测 形式化验证 标记范式图 分布式计算
摘 要：为缓解模型检测的状态空间爆炸问题,提出一种基于命题投影时序逻辑的分布式模型检测方法。通过标记范式图技术将命题投影时序逻辑公式描述的待验证性质转换为自动机;根据强连通分量将其状态空间划分为多个子自动机,将各个子自动机与层次语法图描述的待验证系统模型分发至验证服务器集群中,使用动态验证技术进行多机协同完成系统模型检测验证。实验结果表明,该方法和单机模型检测相比验证时间明显降低,且能够验证更复杂的系统。
维普期刊数据库
同方期刊数据库