Heuristic Symbolic Verification of Safety Properties for Parameterized Systems
Affiliation:

  • Article
  • | |
  • Metrics
  • |
  • Reference [19]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    A parameterized system is a system that involves numerous instantiations of the same finite-state process, and depends on a parameter which defines its size. The backward reachability analysis has been widely used for verifying parameterized systems against safety properties modeled as a set of upward-closed sets. As in the finite-state case, the verification of parameterized systems also faces the state explosion problem and the success of model checking depends on the data structure used for representing a set of states. Several constraint-based approaches have been proposed to symbolically represent upward-closed sets with infinite states. But those approaches are still facing the symbolic state explosion problem or the containment problem, i.e. to decide whether a set of concrete states represented by one set of constraints is a subset of another set of constraints, which is co-NP complete. As a result, those examples investigated in the literature would be considered of negligible size in finite-state model checking. This paper presents several heuristic rules specific to parameterized systems that can help to mitigate the problem. Experimental results show that the efficiency is significantly improved and the heuristic algorithm is several orders of magnitude faster than the original one in certain cases.

    Reference
    [1] Zuck L, Pnueli A. Model checking and abstraction to the aid of parameterized systems (a survey). Computer Languages, Systems and Structures, 2004,30(3-4):139?169.
    [2] Javier E. Verification of systems with an infinite state space. In: Proc. of the Modeling and Verification of Parallel Processes. New York: Springer-Verlag, 2001. 183?186.
    [3] Apt KR, Kozen DC. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 1986,22(6): 307?309.
    [4] Abdulla PA, Cerans K, Jonsson B, Yih-Kuen T. General decidability theorems for infinite-state systems. In: Proc. of the 11th Annual IEEE Symp. on Logic in Computer Science. IEEE Computer Society, 1996. 313?321.
    [5] Emerson EA, Namjoshi KS. On model checking for non-deterministic infinite-state systems. In: Proc. of the 13th Annual IEEE Symp. on Logic in Computer Science. IEEE Computer Society, 1998. 70?80.
    [6] Javier E, Alain F, Richard M. On the verification of broadcast protocols. In: Proc. of the 14th Annual IEEE Symp. on Logic in Computer Science. IEEE Computer Society, 1999. 352?359.
    [7] German SM, Sistla AP. Reasoning about systems with many processes. Journal of the ACM, 1992,39(3):675?735.
    [8] Finkel A, Ph S. Well-Structured transition systems everywhere! Theoretical Computer Science, 2001,256(1-2):63?92.
    [9] Delzanno G, Podelski A. Constraint-Based deductive model checking. Int’l Journal on Software Tools for Technology Transfer, 2001,3(3):250?270.
    [10] Delzanno G. Constraint-Based model checking for parameterized synchronous systems. In: Proc. of the 4th Int’l Workshop on Frontiers of Combining Systems. Springer-Verlag, 2002. 72?86.
    [11] Delzanno G, Raskin JF. Symbolic representation of upward-closed sets. In: Proc. of the 6th Int’l Conf. on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conf. on the Theory and Practice of Software, ETAPS 2000. Springer-Verlag, 2000. 426?440.
    [12] Delzanno G. Constraint-Based verification of parameterized cache coherence protocols. Formal Methods in System Design, 2003, 23(3):257?301.
    [13] Delzanno G, Esparza J, Podelski A. Constraint-Based analysis of broadcast protocols. In: Proc. of the 13th Int’l Workshop and 8th Annual Conf. of the EACSL on Computer Science Logic. Springer-Verlag, 1999. 72?86.
    [14] Bingham JD. A new approach to upward-closed set backward reachability analysis. Electronic Notes in Theoretical Computer Science, 2005,138(3):37?48.
    [15] Delzanno G, Raskin JF, Begin LV. Attacking symbolic state explosion. In: Proc. of the 13th Int’l Conf. on Computer Aided Verification. Springer-Verlag, 2001. 298?310.
    [16] Li MS. Assessing 3-D integrated software development processes: A new benchmark. In: Wang Q, Pfahl D, Raffo DM, Wernick P, eds. Proc. of the SPW/ProSim 2006. LNCS 3966, Shanghai: Springer-Verlag, 2006. 15?38.
    [17] Li MS. Expanding the horizons of software development processes: A 3-D integrated methodology. In: Proc. of the SPW 2005. LNCS 3840, Beijing: Springer-Verlag, 2005. 54?67.
    [18] Li MS, Yang Q, Zhai J, Yang G. On mobility of software processes. In: Wang Q, Pfahl D, Raffo DM, Wernick P, eds. Proc. of the SPW/ProSim 2006. LNCS 3966, Shanghai: Springer-Verlag, 2006. 105?114.
    [19] Yang Q, Li MS, Wang Q, Yang G, Zhai J, Li J, Hou L, Yang Y. An algebraic approach for managing inconsistencies in software processes. In: Wang Q, Pfahl D, Raffo DM, eds. Proc. of the ICSP 2007. LNCS 4470, Minneapolis: Springer-Verlag, 2007. 121?133.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

杨秋松,李明树.参数化系统安全性的启发式符号验证.软件学报,2009,20(6):1444-1456

Copy
Share
Article Metrics
  • Abstract:4521
  • PDF: 6513
  • HTML: 0
  • Cited by: 0
History
  • Received:November 12,2007
  • Revised:March 28,2008
You are the first2038072Visitors
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