微信服务号

微信订阅号

2025年3月24日 17:57 星期一
首页 > 过刊浏览>2008年第19卷第5期 >1149-1159
PDF HTML阅读 XML下载 导出引用 引用提醒
构件组合的抽象精化验证
作者:
基金项目:

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 (上海市重点学科建设项目)


Verification of Component Composition Based on Abstraction Refinement
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [19]
    • |
  • 相似文献 [20]
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件抽象的组合建立构件组合的抽象;提出了组合确认定理并给出证明,使反例确认分解为在各构件上对反例投影的确认;通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化.在模型检验构件组合的过程中,不需要为构件组合建立全局的具体状态空间.

    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.

    参考文献
    [1]Clarke E,Grumberg O,Jha S,Lu Y,Veith H.Counterexample-guided abstraction refinement.In:Emerson EA,Sistla AP,eds.Proc.of the Int'l Conf.on Computer Aided Verification (CAV 2000).LNCS 1855,Heidelberg:Springer-Verlag,2000.154-169.
    [2]Ball T,Majumdar R,Millstein T,Rajamani SK.Automatic predicate abstraction of C programs.ACM SIGPLAN Notices,2001,36(5):203-213.
    [3]Ball T,Rajamani SK.Automatically validating temporal safety properties of interfaces.In:Matthew BD,ed.Proc.of the 8th Int'l SPIN Workshop on Model Checking of Software.LNCS 2057,Heidelberg:Springer-Verlag,2001.103-122.
    [4]Henzinger TA,Jhala R,Majumdar R,Sutre G.Lazy abstraction.ACM SIGPLAN Notices,2002,37(1):58-70.
    [5]Henzinger TA,Jhala R,Majumdar R,Qadeer S.Thread-Modular abstraction refinement.In:Jr Hunt WA,Somenzi F,eds.Proc.of the 15th Int'l Conf.on Computer Aided Verification (CAV 2003).LNCS 2725,Springer-Verlag,2003.262-274.
    [6]Henzinger TA,Jhala R,Majumdar R,Sutre G.Software verification with BLAST.In:Ball T,Rajamani SK,eds.Proc.of the 10th Int'l SPIN Workshop.LNCS 2648,Heidelberg:Springer-Verlag,2003.235-239.
    [7]Grumberg O,Long DE.Model checking and modular verification.ACM Trans.on Programming Languages and Systems,1994,16(3):843-871.
    [8]Corbett JC,Dwyer MB,Hatcliff J,Laubach S,P-s-reanu CS,Robby,Zheng HJ.Bandera:Extracting finite-state models from Java source code.In:Proc.of the 22nd Int'l Conf.on Software Engineering (ICSE 2000).New York:ACM Press,2000.439-448.
    [9]P-s-reanu CS,Dwyer MB,Visser W.Finding feasible counter-examples when model checking abstracted Java programs.In:Margaria T,Wang Y,eds,Proc.of the 7th Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001).LNCS 2031,Heidelberg:Springer-Verlag,2001.284-298.
    [10]He F,Song XY,Gu M,Sun JG.Effective heuristics for counterexample-guided abstraction refinement.In:Proc.of the 17th Great Lakes Symp.on Great Lakes Symp.on VLSI.2007.393-398.
    [11]Chaki S,Clarke EM,Groce A,Jha S,Veith H.Modular verification of software components in C.IEEE Trans.on Software Engineering,2004,30(6):388-402.
    [12]Brandin BA,Malik R,Malik P.Incremental verification and synthesis of discrete-event systems guided by counter examples.IEEE Trans.on Control Systems Technology,2004,12(3):387-401.
    [13]Berezin S,Campos S,Clarke EM.Compositional reasoning in model checking.In:Langmaack H,Pnueli A,de Roever WP,eds.Proc of the Int'l Symp.on Compositionality (COMPOS'97).LNCS 1536,Heidelberg:Springer-Verlag,1998.81-102.
    [14]Henzinger TA,Qadeer S,Rajamani SK.Decomposing refinement proofs using assume-guarantee reasoning.In:Sentovich E,ed.Proc.of the 2000 Int'l Conf.on Computer-Aided Design (ICCAD 2000).IEEE Computer Society Press,2000.245-252.
    [15]Cobleigh JM,Giannakopoulou D,P-s-reanu CS.Learning assumptions for compositional verification.In:Garavel H,Hatcliff J,eds.Proc.of the 9th Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003).LNCS 2619,Heidelberg:Springer-Verlag,2003.331-346.
    [16]Wen YJ,Wang J,Qi ZC.Compositional model checking and compositional refinement checking of concurrent reactive systems.Journal of Software,2007,18(6):1270-1281 (in Chinese with English abstract).http://www.jos.org.cn/1000-9825/18/1270.htm
    [17]Hu J,Yu XF,Zhang Y,Wang LZ,LI XD,Zheng GL.Checking component-based designs for scenario-based specifications.Chinese Journal of Computers,2006,29(4):513-525 (in Chinese with English abstract).
    [18]Lee EA,Xiong YH.System-Level types for component-based design.In:Henzinger TA,Kirsch CM,eds.Proc.of the EMSOFT 2001.LNCS 2211,Heidelberg:Springer-Verlag,2001.237-253.
    [19]Bultan T,Fu X,Hull R,Su JW.Conversation specification:A new approach to design and analysis of e-service composition.In:WWW 2003,Proc.of the 12th Int'l Conf.on World Wide Web.New York:ACM,2003.403-410.
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

曾红卫,缪淮扣.构件组合的抽象精化验证.软件学报,2008,19(5):1149-1159

复制
分享
文章指标
  • 点击次数:7627
  • 下载次数: 8459
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2007-11-15
  • 最后修改日期:2008-03-11
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19728452位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号