A meta-theory for component interfaces with contracts on ports

被引:3
作者
Bauer, Sebastian [1 ]
Hennicker, Rolf [1 ]
Legay, Axel [2 ]
机构
[1] Univ Munich, D-81377 Munich, Germany
[2] INRIA IRISA Rennes, Rennes, France
关键词
Interface specifications; Contracts; Refinement; Compatibility; Modal I/O-transition systems; ASSUME-GUARANTEE VERIFICATION; MODEL CHECKING; REFINEMENT; BEHAVIOR;
D O I
10.1016/j.scico.2013.09.013
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We show how the abstract concept of a labeled interface theory can be canonically extended to an abstract framework for component interfaces with ports. The resulting theory satisfies itself the general laws of an interface theory for composition, refinement and communication compatibility. The ports of a component interface represent the interaction points of a component. Each port is equipped with a contract specifying the assumptions on and the guarantees for the environment of a component. We study reliable component interfaces and we provide methodological guidelines how to design reliable interfaces and how to adapt them to changing environments. Two instances of our approach are presented. First, we consider modal component interfaces such that component behaviors and the assume and guarantee behaviors of ports are given in terms of modal I/O-transition systems with weak notions of refinement and compatibility. The second instance uses I/O-predicates as interface specifications. (C) 2013 Elsevier B.V. All rights reserved.
引用
收藏
页码:70 / 89
页数:20
相关论文
共 42 条
[1]  
Allen R., 1997, ACM Transactions on Software Engineering and Methodology, V6, P213, DOI 10.1145/258077.258078
[2]  
[Anonymous], 2001, LNCS, DOI [DOI 10.1007/3-540-45449-7_11, DOI 10.1007/3-540-45449-711]
[3]  
Back R.-J., 1999, REFINEMENT CALCULUS
[4]   Rigorous Component-Based System Design Using the BIP Framework [J].
Basu, Ananda ;
Bensalem, Saddek ;
Bozga, Marius ;
Combaz, Jacques ;
Jaber, Mohamad ;
Thanh-Hung Nguyen ;
Sifakis, Joseph .
IEEE SOFTWARE, 2011, 28 (03) :41-48
[5]  
Bauer SS, 2012, LECT NOTES COMPUT SC, V7212, P43, DOI 10.1007/978-3-642-28872-2_3
[6]   Interface theories for concurrency and data [J].
Bauer, Sebastian S. ;
Hennicker, Rolf ;
Wirsing, Martin .
THEORETICAL COMPUTER SCIENCE, 2011, 412 (28) :3101-3121
[7]   Interface Theories for (A) synchronously Communicating Modal I/O-Transition Systems [J].
Bauer, Sebastian S. ;
Hennicker, Rolf ;
Janisch, Stephan .
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (46) :1-8
[8]  
Bauer SS, 2010, LECT NOTES COMPUT SC, V6015, P175, DOI 10.1007/978-3-642-12002-2_15
[9]  
Bauer Sebastian S., 2012, THESIS LUDWIG MAXIMI
[10]  
Bauer Sebastian S., 2012, LECT NOTES COMPUT SC, V7684, P19