attacking the dimensionality problem of parameterized systems via bounded reachability graphs

ISCAS OpenIR

	attacking the dimensionality problem of parameterized systems via bounded reachability graphs
	Yang Qiusong; Zhang Bei; Zhai Jian; Li Mingshu
	2012
会议名称	4th IPM International Conference on Fundamentals of Software Engineering, FSEN 2011
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	221-235
会议日期	April 20, 2011 - April 22, 2011
会议地点	Tehran, Iran
收录类别	EI ; SPRINGER
ISSN	0302-9743
ISBN	9783642293191
部门归属	(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
摘要	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.; 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.
关键词	Abstracting Parameterization
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15732
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Yang Qiusong,Zhang Bei,Zhai Jian,et al. attacking the dimensionality problem of parameterized systems via bounded reachability graphs[C],2012:221-235.