| 构件组合的抽象精化验证 |
| |
| 引用本文： | 曾红卫,缪淮扣.构件组合的抽象精化验证[J].软件学报,2008,19(5):1149-1159. |
| |
| 作者姓名： | 曾红卫 缪淮扣 |
| |
| 作者单位： | 上海大学,计算机工程与科学学院,上海,200072 |
| |
| 基金项目： | Supported by the National Natural Science Foundation of China under Grant No.60673115 (国家自然科学基金); the National High-Tech Research and Development Plan of China under Grant No.2007AA01Z144 (国家高技术研究发展计划(863)); the National Basic Research Program of China under Grant Nos.2007CB310800, 2002CB312001 (国家重点基础研究发展计划(973)); the Research Program of Shanghai Education Committee of China under Grant No.07ZZ06 (上海市教委科研项目); the Shanghai Leading Academic Discipline Project of China under Grant No.J50103 (上海市重点学科建设项目) |
| |
| 摘 要： | 针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件抽象的组合建立构件组合的抽象;提出了组合确认定理并给出证明,使反例确认分解为在各构件上对反例投影的确认;通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化.在模型检验构件组合的过程中,不需要为构件组合建立全局的具体状态空间.
|
| 关 键 词： | 构件组合 模型检验 状态爆炸 等价关系 反例引导的抽象精化 |
| 收稿时间： | 2007/11/15 0:00:00 |
| 修稿时间： | 2007年11月15 |
Verification of Component Composition Based on Abstraction Refinement |
| |
| ZENG Hong-Wei and MIAO Huai-Kou.Verification of Component Composition Based on Abstraction Refinement[J].Journal of Software,2008,19(5):1149-1159. |
| |
| Authors: | ZENG Hong-Wei and MIAO Huai-Kou |
| |
| Abstract: | This paper addresses the state-space explosion problem in the context of verifying component composition.It adapts the counterexample guided abstraction refinement (CEGAR) scheme and proposes a compositional verification approach that the verification of component composition is transformed into local abstraction refinement for individual components participating in the composition in order to reduce analysis complexity.The existential quotient based on equivalence relation is employed to compute the abstraction of each component in component composition,and then the abstraction model for the component composition can be built by composing the existential quotients of components.A compositional validation theorem is proposed and proved, so validating if a generated counterexample is valid and refining the abstraction are all carried out component-wise. This approach does not require the construction of a complete state space of the concrete component composition under verification. |
| |
| Keywords: | component composition model checking state explosion equivalence relation counterexample guided abstraction refinement |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
