Common use of Extended Component Model Clause in Contracts

Extended Component Model. ‌ In our approach, metadata comprise information that can (at any moment) be derived from other component contract elements. Such metadata enriches component contracts with static information that assists the runtime envi- ronment with additional (validation) properties. The metadata information is: (1) dual protocols; (2) context protocols; (3) protocol implementations; and (4) decoupled channels. Informally, the behaviour of the dual protocol of a process P after a trace s is always an external choice of the outputs and one of the inputs of P , if it exists, after s. Furthermore, a context protocol of a process P is a deadlock-free deterministic process that has the same traces as P . Both are used in protocol compatibility verifications. The main metadata information selected in our approach are decoupled channels and protocol implementations. These are important conditions in the communi- cation and feedback compositions rules. Similarly to the composition rules presented before, we presented four composition rules for enriched component contracts. In particular, we use metadata to alleviate several verifications in our rigorous strategy for component compositions. The extended contracts specialise the notion of protocol oriented component and enrich their contract with metadata. (BCtr, RCtr, ICtr, CCtr, K) where K comprises the following information: K : (Prot K, CTXK, DProt K, DecK) such that: • dom Prot K ⊆ CCtr ∧ ∀ c : dom Prot K • Prot K(c) ±F ProtIMP (Ctr, c) • dom DProt K ⊆ CCtr ∧ ∀ c : dom DProt K • DProt K(c) is the dual protocol of Prot K(c) • dom CTXK ⊆ CCtr ∧ ∀ c : dom CTXK • CTXK(c) is the context process of Prot K(c) • dom DecK ⊆ CCtr ∧ ran DecK ⊆ CCtr • ∀ c1, c2 : CCtr • c1 DecK c2 ⇒ {c1, c2} DecoupledIn Ctr ∧ c2 DecK c1 The element Prot K is a relation from channels to protocols, which represent the actual port-protocol of the component on that channel. If a protocol within Prot K satisfies a property, then, by refinement, it also holds for the protocol of the component. Similarly, the elements DProt K and CTXK map channels into context processes and dual protocols, respectively. They are used to support the use of the protocols within Prot K; these are used, for instance, in protocol compatibility verifications. Finally the element DecK is a relation among decoupled channels of the component. Since these metadata comprise derived information, it can be ignored by a composition environment, and, furthermore, the component can still be used in environments unaware of them. As a consequence, despite the use of metadata can be considered a powerful tool during the integration phase, its use is optional. To increase the value of our compositional approach, we derive composition metadata from the metadata of the original components, without always building them from scratch. After each composition rule is applied, the metadata are updated using simple formulae that consider the semantics of such composition rule. Similarly to the composition rules presented before, we present four compo- sition rules for enriched component contracts. In order to preserve protocols behaviours after each composition and to store them in metadata, enriched components require a stronger verification of protocol compatibility, which we call matching compatible. Similarly to the rules presented before, we present four new composition rules for enriched component contracts. In order to preserve protocol behaviours after each composition and to store them in metadata, the new rules require a stronger notion of protocol compatibility, which we call matching compat- ibility.