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 |
| 会议日期 | April 20, 2011 - April 22, 2011 |
| 会议地点 | Tehran, Iran |
| 关键词 | Abstracting Parameterization |
| 页码 | 221-235 |
| 中文摘要 | 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. |
| 收录类别 | EI ; SPRINGER |
| 会议录 | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
 |
| 语种 | 英语 |
| ISSN号 | 0302-9743 |
| ISBN号 | 9783642293191 |
| 源URL | [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]. 见:4th IPM International Conference on Fundamentals of Software Engineering, FSEN 2011. Tehran, Iran. April 20, 2011 - April 22, 2011. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。