一种基于构件演算的主动构件精化方法
作者:
基金项目:

Supported by the National Basic Research Program of China under Grant No.2002CB312001 (国家重点基础研究发展计划(973)); the National High-Tech Research and Development Plan of China under Grant No.2007AA010302 (国家高技术研究发展计划(863)); the Natural Science Foundation of Jiangsu Province of China under Grant No.BK2007714 (江苏省自然科学基金)


An Approach to Refining Active Components Based on Component Calculus
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [13]
  • |
  • 相似文献 [20]
  • |
  • 引证文献
  • | |
  • 文章评论
    摘要:

    现代构件系统通常包含多个并发执行的主动构件,这使得验证构件系统的正确性变得十分困难.通过对构件演算进行扩展,提出了一种主动构件的精化方法.在构件接口层引入契约.契约使用卫式设计描述公共方法和主动活动的功能规约.通过一对发散、失败集合定义契约的动态行为,并利用发散、失败集合之间的包含关系定义契约间的精化关系.证明了应用仿真技术确认契约精化关系的定理.定义构件的语义为其需求接口契约到其服务接口契约的函数,以此为基础,可以通过契约的精化来证明构件的精化.给出了构件的组装规则.在构件系统自底向上的构造过程中,应用构件的精化方法和组装规则可以保证最终系统的正确性.

    Abstract:

    Modern component-based systems consist of active components that execute in parallel, which brings great difficulties in verifying correctness. By extending component calculus, a theory concerning refinement of active components is proposed. For interfaces, contracts are introduced which give functional specifications for both public methods and active action in terms of guarded designs. Then, a contract's dynamic behavior is defined by a pair of divergences/failures sets. The refinement relation between contracts is defined as the set inclusion of their divergences/failures sets. The theories applying simulation techniques to assure the refinement relation are proved. By defining the semantics of a component as a mapping from the contract of its required interface to the contract of its provide interface, component refinement can be proved in terms of contract refinement. When the component- based systems are being constructed in a bottom-up manner, the application of the refinement method together with the composition rule can guarantee their correctness.

    参考文献
    [1]Morgan C.Programming form Specifications.Hemel Hempstead:Prentice-Hall,Inc.,1998.163-179.
    [2]He JF,Li XS,Liu ZM.rCOS:A refinement calculus of object systems.Theoretical Computer Science,2006,365(2):109-142.
    [3]Hoare CAR,He JF.Unifying Theories of Programming.London:Prentice-Hall,Inc.,1998.74-85.
    [4]He JF,Li XS,Liu ZM.A theory of reactive components.Electronic Notes in Theoretical Computer Science,2006,160:173-195.
    [5]Roscoe AW.Theory and Practice of Concurrency.London:Prentice-Hall,Inc.,1997.519-553.
    [6]Bergner K,Rausch A,Sihling M,Vilbig A,Broy M.Foundations of Component-Based Systems.New York:Cambridge University Press.2000.189-210.
    [7]Hu J,Yu XF,Zhang Y,Zhang T,Wang LZ,Li XD,Zheng GL.Scenario-Based specifications verification for component-based embedded software designs.In:Proc.of the ICPP 2005 Workshops.IEEE Computer Society,2005.240-247.
    [8]Gossler G,Sifakis J.Composition for component-based modeling.In:de Boer FS,Bonsangue MM,Graf S,de Roever WP,eds.Proc.of the FMCO 2002.LNCS 2852,Heidelberg:Springer-Verlag,2003.443-466.
    [9]Arbab F.Abstract behavior types:A foundation model for components and their composition.In:de Boer FS,Bonsangue MM,Graf S,de Roever WP,eds.Proc.of the FMCO 2002.LNCS 2852,Heidelberg:Springer-Verlag,2003.33-70.
    [10]Chouali S,Heisel M,Souquières.Proving component interoperability with B refinement.Electronic Notes in Theoretical Computer Science,2006,160:157-172.
    [11]Xie F,Browne JC.Verified systems by composition from verified components.In:Proc.of the ESEC/SIGSOFT FSE 2003.New York:ACM,2003.277-286.
    [12]Liu J,He JF,Liu ZM.A strategy for services realization in service-oriented design.Science in China (Series F),2006,49(6):864-884.
    [13]Chen X,He JF,Liu ZM,Zhan NJ.A model of component-based programming.In:Arbab F,Sirjani M,eds.Proc.of the FSEN 2007.LNCS 4767,Heidelberg:Springer-Verlag,2007.191-206.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

陈 鑫.一种基于构件演算的主动构件精化方法.软件学报,2008,19(5):1134-1148

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2007-11-15
  • 最后修改日期:2008-02-19
文章二维码
您是第19728414位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号