Heuristic Symbolic Verification of Safety Properties for Parameterized Systems
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • 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
    Related
    Cited by
Get Citation

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

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