主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
曾红卫,缪淮扣.构件组合的抽象精化验证.软件学报,2008,19(5):1149-1159
构件组合的抽象精化验证
Verification of Component Composition Based on Abstraction Refinement
投稿时间:2007-11-15  修订日期:2008-03-11
DOI:
中文关键词:  构件组合  模型检验  状态爆炸  等价关系  反例引导的抽象精化
英文关键词:component composition  model checking  state explosion  equivalence relation  counterexample guided abstraction refinement
基金项目: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 (上海市重点学科建设项目)
作者单位
曾红卫 上海大学 计算机工程与科学学院,上海 200072 
缪淮扣 上海大学 计算机工程与科学学院,上海 200072 
摘要点击次数: 5180
全文下载次数: 4015
中文摘要:
      针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件抽象的组合建立构件组合的抽象;提出了组合确认定理并给出证明,使反例确认分解为在各构件上对反例投影的确认;通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化.在模型检验构件组合的过程中,不需要为构件组合建立全局的具体状态空间.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利