中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 会议论文
Title:
attacking the dimensionality problem of parameterized systems via bounded reachability graphs
Author: Yang Qiusong ; Zhang Bei ; Zhai Jian ; Li Mingshu
Source: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Conference Name: 4th IPM International Conference on Fundamentals of Software Engineering, FSEN 2011
Conference Date: April 20, 2011 - April 22, 2011
Issued Date: 2012
Conference Place: Tehran, Iran
Keyword: Abstracting ; Parameterization
Indexed Type: EI ; SPRINGER
ISSN: 0302-9743
ISBN: 9783642293191
Department: (1) National Engineering Research Center of Fundamental Software Institute of Software Chinese Academy of Sciences Beijing 100190 China; (2) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing 100190 China; (3) Graduate University Chinese Academy of Sciences Beijing 100039 China
Abstract: Parameterized systems are systems that involve numerous instantiations of finite-state processes, and depend on parameters which define their size. The verification of parameterized systems is to decide if a property holds in its every size instance, essentially a problem with an infinite state space, and thus poses a great challenge to the community. Starting with a set of undesired states represented by an upward-closed set, the backward reachability analysis will always terminate because of the well-quasi-orderingness. As a result, backward reachability analysis has been widely used in the verification of parameterized systems. However, many existing approaches are facing with the dimensionality problem, which describes the phenomenon that the memory used for storing the symbolic state space grows extremely fast when the number of states of the finite-state process increases, making the verification rather inefficient. Based on bounded backward reachability graphs, a novel abstraction for parameterized systems, we have developed an approach for building abstractions with incrementally increased dimensions and thus improving the precision until a property is proven or a counterexample is detected. The experiments show that the verification efficiencies have been significantly improved because conclusive results tend to be drawn on abstractions with much lower dimensions. © 2012 Springer-Verlag.
English Abstract: Parameterized systems are systems that involve numerous instantiations of finite-state processes, and depend on parameters which define their size. The verification of parameterized systems is to decide if a property holds in its every size instance, essentially a problem with an infinite state space, and thus poses a great challenge to the community. Starting with a set of undesired states represented by an upward-closed set, the backward reachability analysis will always terminate because of the well-quasi-orderingness. As a result, backward reachability analysis has been widely used in the verification of parameterized systems. However, many existing approaches are facing with the dimensionality problem, which describes the phenomenon that the memory used for storing the symbolic state space grows extremely fast when the number of states of the finite-state process increases, making the verification rather inefficient. Based on bounded backward reachability graphs, a novel abstraction for parameterized systems, we have developed an approach for building abstractions with incrementally increased dimensions and thus improving the precision until a property is proven or a counterexample is detected. The experiments show that the verification efficiencies have been significantly improved because conclusive results tend to be drawn on abstractions with much lower dimensions. © 2012 Springer-Verlag.
Language: 英语
Content Type: 会议论文
URI: http://ir.iscas.ac.cn/handle/311060/15732
Appears in Collections:软件所图书馆_会议论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
Yang Qiusong,Zhang Bei,Zhai Jian,et al. attacking the dimensionality problem of parameterized systems via bounded reachability graphs[C]. 见:4th IPM International Conference on Fundamentals of Software Engineering, FSEN 2011. Tehran, Iran. April 20, 2011 - April 22, 2011.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[Yang Qiusong]'s Articles
[Zhang Bei]'s Articles
[Zhai Jian]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Yang Qiusong]‘s Articles
[Zhang Bei]‘s Articles
[Zhai Jian]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace