@inproceedings{GQ07,
title = { Contracts for {BIP}: hierarchical interaction models for compositional verification },
author = {Graf, Susanne and Quinton, Sophie},
year = {2007},
booktitle = {FORTE 2007, Talinn},
note = {invited presentation},
series = {LNCS},
volume = {4574},
team = {DCS},
abstract = {This paper presents an extension of the BIP component framework to hierarchical components by considering also port sets of atomic components to be structured (ports may be in conflict or ordered, where a larger port represents an interaction set with larger interactions). A composed component consisting of a set of components connected through BIP connectors and a set of ports representing a subset of the internal connectors and ports, has two semantics: one in terms if interactions as defined by the BIP semantics, and one in terms of the actions represented by external ports where the structure of the port set of the component is derived from the internal structure of the component. A second extension consists in the addition of implicit interactions which is done through an explicit distinction of conflicting and concurrent ports: interactions involving only non conflicting ports can be executed concurrently without the existence of an explicit connector. Finally, we define contract-based reasoning for component hierarchies. <i>A</i> component <i>K</i> satisfies a contract <i>(A,G)</i> consisting of an assumption <i>A</i> (constraining the environment) and a guarantee <i>G</i> (constraining <i>K</i>), if its implementation satisfies <i>G</i> in an environment guaranteeing <i>A</i>. The contract <i>(A,G)</i> of a component <i>K</i> dominates a set of inner contracts <i>(Ai,Gi)</i> associated with the components defining it, if the composition -- according to the set of connectors defining <i>K</i> --- of the guarantees <i>Gi</i> in the environment defined by <i>A</i> gurantees <i>G</i>, and, if each of the assumptions <i>Ai</i> is weaker than the one defined by the composition of <i>A</i> with the remaining guarantees. This rule is consistent because <i>G</i> expresses a safety property of <i>K</i> only, and not of the closed system obtained by composing <i>A</i> and <i>K</i>},
}
