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

Implementation and Optimization of Multi-Core Model Checker CTAV
Author:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [19]
  • |
  • 相似文献
  • | | |
  • 文章评论
    摘要:

    在计算机计算能力大大增强的时代,为了提高对时间自动机进行空性检测的效率,进一步高效利用多核处理器的优势,研究了利用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.

    参考文献
    1 Clarke EM, Grumberg O, Peled DA. Model Checking. The MIT Press, 1999.
    2 Li GY. Checking timed Büchi automata emptiness using LU-abstractions. Proceedings of the 7th International Conference on Formal Modeling and Analysis of Timed Systems. 2009:228-242.
    3 http://lcs.ios.ac.cn/~ligy/tools/CTAV_LTL/.
    4 Laarman A, Olesen MC, Dalsgaard AE, et al. Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. In:Sharygina N, Veith H, eds. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer. Berlin, Heidelberg. 2013. 968-983.[doi:10.1007/978-3-642-39799-8_69]
    5 Laarman A, Langerak R, van de Pol J, et al. Multi-core nested depth-first search. In:Bultan T, Hsiung PA, eds. Automated Technology for Verification and Analysis. ATVA 2011. Lecture Notes in Computer Science, vol 6996. Springer. Berlin, Heidelberg. 2011. 321-335.[doi:10.1007/978-3-642-24372-1_23]
    6 Evangelista S, Petrucci L, Youcef S. Parallel nested depth-first searches for LTL model checking. In:Bultan T, Hsiung PA, eds. Automated Technology for Verification and Analysis. ATVA 2011. Lecture Notes in Computer Science, vol 6996. Springer. Berlin, Heidelberg. 2011. 381-396.[doi:10.1007/978-3-642-24372-1_27]
    7 Evangelista S, Laarman A, Petrucci L, et al. Improved multi-core nested depth-first search. In:Chakraborty S, Mukund M, eds. Automated Technology for Verification and Analysis. ATVA 2012. Lecture Notes in Computer Science, vol 7561. Springer. Berlin, Heidelberg. 2012. 269-283.[doi:10.1007/978-3-642-33386-6_22]
    8 Barnat J, Brim L, Rockai P. DiVinE multi-core-a parallel LTL model-checker. In:Cha S, Choi JY, Kim M, et al., eds. Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 5311. Springer. Berlin, Heidelberg. 2008. 234-239.[doi:10.1007/978-3-540-88387-6_20]
    9 Barnat J, Brim L, Havel V, et al. DiVinE 3.0-an explicit-state model checker for multithreaded C & C++ programs. In:Sharygina N, Veith H, eds. Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer. Berlin, Heidelberg. 2013. 863-868.[doi:10.1007/978-3-642-39799-8_60]
    10 Renault E, Duret-Lutz A, Kordon F, et al. Parallel explicit model checking for generalized Büchi automata. TACAS'15, vol. 9035 of LNCS. Springer. 2015. 613-627.
    11 Renault E, Duret-Lutz A, Kordon F, et al. Variations on parallel explicit emptiness checks for generalized büchi automata. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2017, 19(6):653-673.[doi:10.1007/s10009-016-0422-5]
    12 Renault E, Duret-Lutz A, Kordon F, et al. Three SCC-based emptiness checks for generalized Büchi automata. In:McMillan K, Middeldorp A, Voronkov A, eds. Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. 2013. 668-682.[doi:10.1007/978-3-642-45221-5_44]
    13 Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994, 126(2):183-226.[doi:10.1016/0304-3975(94)90010-8]
    14 晏荣杰. 基于整数时间的实时系统符号化模型检测技术[博士学位论文]. 北京:中国科学院软件研究所, 2007.
    15 Henzinger TA, Nicollin X, Sifakis J, et al. Symbolic model checking for real-time systems. Journal of Information and Computation, 1994, 111(2):193-244.[doi:10.1006/inco.1994.1045]
    16 Bengtsson J, Yi W. Timed automata:Semantics, algorithms and tools. In:Desel J, Reisig W, Rozenberg G, eds. Lectures on Concurrency and Petri Nets. ACPN 2003. Lecture Notes in Computer Science, vol 3098. Springer, Berlin, Heidelberg. 2004. 87-124.[doi:10.1007/978-3-540-27755-2_3]
    17 Tarjan R. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1972, 1(2):146-160.[doi:10.1137/0201010]
    18 Dijkstra EW. EWD 376:Finding the maximum strong components in a directed graph. http://www.cs.utexas.edu/users/EWD/ewd03xx/WD376.PDF.[1973-05].
    19 Ruiz V, Diaz G, Cambronero ME. Timed automata modeling and verification for publish-subscribe structures using distributed resources. IEEE Transactions on Software Engineering, 2017, 43(1):76-99[doi:10.1109/TSE.2016.2560842]
    相似文献
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

赵威.多核模型检测工具CTAV的实现与优化.计算机系统应用,2018,27(9):176-181

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2018-02-01
  • 最后修改日期:2018-02-28
  • 在线发布日期: 2018-08-17
文章二维码
您是第12435498位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京海淀区中关村南四街4号 中科院软件园区 7号楼305房间,邮政编码:100190
电话:010-62661041 传真: Email:csa (a) iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号