Component Composition Preserving Behavioural Contracts Based on Communication Traces
Résumé
This paper investigates the compositional properties of reu- sable software components defined with explicit dependencies and be- havioural contracts expressing rely-guarantee specifications in the form of communication traces. In this setting, connection of components through their matching ports is indeed compositional and yields a new component or composite that respects its constituents' contracts. Thus the behaviour of the composite is computed from the behaviours of its constituents and is known to conform to the contracts without any new proof.