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

Implementation and Optimization of Multi-Core Model Checker CTAV

作　　者：赵威 ZHAO Wei(State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100190,China;University of Chinese Academy of Sciences,Beijing 100049,China)

机构地区：[1]中国科学院软件研究所计算机科学国家重点实验室 [2]中国科学院大学

出　　处：《计算机系统应用》2018年第9期176-181,共6页Computer Systems & Applications

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

关 键 词：时间自动机 线性时序逻辑 多核并行模型检测 符号化状态 

分 类 号：TP391.7[自动化与计算机技术—计算机应用技术]