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

• 作者: 张丽丽 王昌太 王燕 舒新峰
• 来源期刊: 西安电子科技大学学报（自然科学版）
• 学科: 工学
• 关键词: 命题投影时序逻辑 模型检测 形式化验证 标记范式图 分布式计算
• 年，卷（期）: 2020,（4）
• 页码范围: 39-47
• 页数: 9页
• 分类号: TP302.7
• 字数: 5469字
• 语种: 中文
• DOI: 10.19665/j.issn1001-2400.2020.04.006

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	舒新峰	西安邮电大学计算机学院	23	48	4.0	6.0
2	王燕	西安邮电大学计算机学院	7	6	2.0	2.0
3	张丽丽	西安邮电大学计算机学院	6	5	1.0	1.0
4	王昌太	西安邮电大学计算机学院	2	0	0.0	0.0