微信服务号

微信订阅号

2025-5-16- 2
Home > Archive>Volume 20, Issue 8, 2009 >2005-2014
PDF HTML XML Export Cite reminder
Optimization of Bounded Model Checking
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [15]
    • |
  • Related [20]
    • |
  • Cited by [2]
    • | |
  • Comments
    Abstract:

    This paper optimizes the encoding of verifying G(p) and G(p→F(q)) which are two important and frequently used modal operators in optimization of encoding for bounded model checking (BMC). Through analysis of the properties of finite state machine (FSM) and LTL (linear-time temporal logic) when verifying these modal operators, it presents a concise recursive formula, which can efficiently translate BMC instances into SAT (satisfiability) instances. The logical properties of these recursion formulas are verified. The experimental comparison between the optimization of BMC and the other two important methods AA_BMC and Timo_BMC for solving these modal operators in BMC shows that the former is superior to the latter in both the scale of instances and the difficulty to solve the problem. Research of this paper is also beneficial to encoding optimization of verifying other modal operators in BMC.

    Reference
    [1] Clarke EM, Grumberg O, Peled DA. Model Checking. Cambridge: The MIT Press, 1999. 61?87.
    [2] Biere A, Cimatti A, Clarke EM, Zhu Y. Symbolic model checking without BDDs. In: Cleaveland R, ed. Proc. of the 5th Int’l Conf. on Tools and Algorithms for the Constructions and Analysis of Systems (TACAS’99). LNCS 1579, Berlin: Springer-Verlag, 1999. 193?207.
    [3] Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A. NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma E, Larsen KG, eds. Proc. of the 14th Int’l Conf. on Computer Aided Verification(CAV 2002). LNCS 2404, Berlin: Springer-Verlag, 2002. 359?364.
    [4] Amla N, Kurshan R, McMillan K, Medel R. Experimental analysis of different techniques for bounded model checking. In: Hubert G, Hatcliff J, eds. Proc. of the 9th Int’l Conf. on Tools and Algorithms for the Constructions and Analysis of Systems (TACAS 2003). LNCS 2619, Berlin: Springer-Verlag, 2003. 34?48.
    [5] Luo XY, Su KL, Yang JJ. Bounded model checking for temporal epistemic logic in synchronous multi-agent systems. Journal of Software, 2006,17(12):2485?2498 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/17/2485.htm
    [6] Daniel G, Ulrich K, Rolf D. HW/SW co-verification of embedded systems using bounded model checking. In: Qu G, Ismail YI, Vijaykrishnan N, Zhou H, eds. Proc. of the 16th ACM Great Lakes Symp. on VLSI 2006. Cairns: ACM Press, 2006. 43?48.
    [7] Cimatti A, Pistore M, Roveri M, Sebastiani R. Improving the encoding of LTL model checking into SAT. In: Agostino C, ed. Proc. of the 3rd Int’l Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI 2002). LNCS 2294, Berlin: Springer-Verlag, 2002. 196?207.
    [8] Frisch A, Sheridan D, Walsh T. A fixpoint encoding for bounded model checking. In: Aagaard MD, OLeary JW, eds. Proc. of the 4th Int’l Conf. on Formal Methods in Computer-Aided Design (FMCAD 2002). LNCS 2517, Berlin: Springer-Verlag, 2002. 238?255.
    [9] Latvala T, Biere A, Heljanko K, Junttila T. Simple bounded LTL model checking. In: Hu AJ, Martin AK, eds. Proc. of the 5th Int’l Conf. on Formal Methods in Computer-Aided Design (FMCAD 2004). LNCS 3312, Berlin: Springer-Verlag, 2004. 186?200.
    [10] Jackson P, Sheridan D. Clause form conversions for boolean circuits. In: Hoos HH, Mitchell DG, eds. Proc. of the 7th Int’l Conf. on Theory and Applications of Satisfiability Testing (SAT 2004). LNCS 3542, Berlin: Springer-Verlag, 2004. 183?198.
    [11] Jackson P, Sheridan D. The optimality of a fast CNF conversion and its use with SAT. In: Hoos HH, Mitchell DG, eds. Proc. of the 7th Int’l Conf. on Theory and Applications of Satisfiability Testing (SAT 2004). LNCS 3709, Berlin: Springer-Verlag, 2005. 827?831.
    [12] Strichman O. Accelerating bounded model checking of safety properties. Formal Methods in System Design, 2004,24(1):5?24.
    [13] Clarke EM, Kroenig D, Oukanine J, Strichman O. Completeness and complexity of bounded model checking. In: Steffen B, Levi G, eds. Proc. of the 5th Int’l Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI 2004). LNCS 2937, Berlin: Springer-Verlag, 2004. 85?96.
    [14] Gupta A, Ganai M, Wang C, Yang Z, Ashar P. Learning from BDDs in SAT-based bounded model checking. In: Proc. of the 40th Conf. on Design Automation (DAC 2003). Montreal: IEEE Computer Society Press, 2003. 824?829.
    [15] http://nusmv.irst.itc.it/examples/examples.html
    Comments
    Comments
    分享到微博
    Submit
Get Citation

杨晋吉,苏开乐,骆翔宇,林瀚,肖茵茵.有界模型检测的优化.软件学报,2009,20(8):2005-2014

Copy
Share
Article Metrics
  • Abstract:5711
  • PDF: 7643
  • HTML: 0
  • Cited by: 0
History
  • Received:September 29,2007
  • Revised:April 15,2008
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2044807Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063