多核模型检测工具CTAV的实现与优化

• 作者: 赵威
• 来源期刊: 计算机系统应用
• 关键词: 时间自动机 线性时序逻辑 多核并行模型检测 符号化状态
• 年，卷（期）: 2018,（9）
• 所属期刊栏目: 软件技术·算法
• 页码范围: 176-181
• 页数: 6页
• 字数: 4337字
• 语种: 中文
• DOI: 10.15888/j.cnki.csa.006546

摘要

在计算机计算能力大大增强的时代, 为了提高对时间自动机进行空性检测的效率, 进一步高效利用多核处理器的优势, 研究了利用Büchi自动机的多核空性判定算法改造CTAV, 使它成为一款时间自动机模型关于线性时序逻辑的多核模型检测工具, 从而提高模型检测的效率. 通过对符号化状态之间包含关系的研究, 利用这种状态之间的包含关系更快的找到接收路径并避免不必要的状态展开, 实现了多核模型检测算法的优化, 对比了一些常见模型的验证数据, 取得了更好的效果.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	赵威	中国科学院软件研究所计算机科学国家重点实验室	11	238	6.0	11.0