Moving from Specifications to Contracts in Component-Based Design

被引:0
作者
Bauer, Sebastian S. [1 ]
David, Alexandre [2 ]
Hennicker, Rolf [1 ]
Larsen, Kim Guldstrand [2 ]
Legay, Axel [2 ,3 ]
Nyman, Ulrik [2 ]
Wasowski, Andrzej [4 ]
机构
[1] Univ Munich, Marchioninistr 15, D-81377 Munich, Germany
[2] Aalborg Univ, Dept Comp Sci, Aalborg, Denmark
[3] INRIA, IRISA, Rennes, France
[4] IT Univ Copenhagen, Copenhagen, Denmark
来源
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2012 | 2012年 / 7212卷
关键词
TRANSITION-SYSTEMS;
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We study the relation between specifications of component behaviors and contracts providing means to specify assumptions on environments as well as component guarantees. We show how a contract framework can be built in a generic way on top of any specification theory which supports composition and specification refinement. Our contract framework lifts refinement to the level of contracts and proposes a notion of contract composition on the basis of dominating contracts. Contract composition satisfies a universal property and can be constructively defined if the underlying specification theory is complete, i.e. it offers operators for quotienting and conjoining specifications. We illustrate our generic construction of contracts by moving a specification theory for modal transition systems to contracts and we show that a (previously proposed) trace-based contract theory is an instance of our framework.
引用
收藏
页码:43 / 58
页数:16
相关论文
共 37 条
  • [1] Aarts F, 2010, LECT NOTES COMPUT SC, V6269, P71, DOI 10.1007/978-3-642-15375-4_6
  • [2] Bauer S.S., 2012, 1201 LMU
  • [3] Bauer S.S., 2011, LNCS
  • [4] Bauer SS, 2011, LECT NOTES COMPUT SC, V6907, P60, DOI 10.1007/978-3-642-22993-0_9
  • [5] Bauer SS, 2010, LECT NOTES COMPUT SC, V6015, P175, DOI 10.1007/978-3-642-12002-2_15
  • [6] Bauer SS, 2009, LECT NOTES COMPUT SC, V5728, P367, DOI 10.1007/978-3-642-03741-2_25
  • [7] Benveniste A, 2008, LECT NOTES COMPUT SC, V5382, P200, DOI 10.1007/978-3-540-92188-2_9
  • [8] Bertrand N, 2009, LECT NOTES COMPUT SC, V5885, P679, DOI 10.1007/978-3-642-10373-5_35
  • [9] Constraint Markov Chains
    Caillaud, Benoit
    Delahaye, Benoit
    Larsen, Kim G.
    Legay, Axel
    Pedersen, Mikkel L.
    Wasowski, Andrzej
    [J]. THEORETICAL COMPUTER SCIENCE, 2011, 412 (34) : 4373 - 4404
  • [10] Chakrabarti A, 2003, LECT NOTES COMPUT SC, V2855, P117