###
计算机系统应用:2018,27(9):176-181
本文二维码信息
码上扫一扫!
多核模型检测工具CTAV的实现与优化
赵威1,2
(1.中国科学院 软件研究所 计算机科学国家重点实验室, 北京 100190;2.
中国科学院大学, 北京 100049)
Implementation and Optimization of Multi-Core Model Checker CTAV
ZHAO Wei1,2
(1.State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China;2.
University of Chinese Academy of Sciences, Beijing 100049, China)
摘要
图/表
参考文献
相似文献
本文已被:浏览 70次   下载 71
投稿时间:2018-02-01    修订日期:2018-02-28
中文摘要: 在计算机计算能力大大增强的时代,为了提高对时间自动机进行空性检测的效率,进一步高效利用多核处理器的优势,研究了利用Büchi自动机的多核空性判定算法改造CTAV,使它成为一款时间自动机模型关于线性时序逻辑的多核模型检测工具,从而提高模型检测的效率.通过对符号化状态之间包含关系的研究,利用这种状态之间的包含关系更快的找到接收路径并避免不必要的状态展开,实现了多核模型检测算法的优化,对比了一些常见模型的验证数据,取得了更好的效果.
Abstract:In the era of the increased computation capacity of computer, in order to improve the efficiency of checking emptiness of timed automaton, and make more efficient using of the advantages of multi-core processors, we use multi-core emptiness checking algorithm of timed Büchi automata to rebuild CTAV, making it become a multi-core model checker for linear temporal logic, which improves the efficiency of model checking. Since there are equivalence and inclusion relationship between symbolic states, by making use of this relationship, a model checker can find accepted path faster and avoid unnecessary state explorations. Thus, checking takes less time. Finally, the effectiveness of presented method is demonstrated by case study.
文章编号:     中图分类号:    文献标志码:
基金项目:
引用文本:
赵威.多核模型检测工具CTAV的实现与优化.计算机系统应用,2018,27(9):176-181
ZHAO Wei.Implementation and Optimization of Multi-Core Model Checker CTAV.COMPUTER SYSTEMS APPLICATIONS,2018,27(9):176-181

用微信扫一扫

用微信扫一扫