Behaviour Protocols for Interacting Stateful Components

We propose a formal foundation for behaviour protocols of interacting, concurrent components with data states. Formally, behaviour protocols are given by labelled transition systems which specify the order of operation invocations as well as the allowed changes of data states of components in terms of pre- and postconditions. We study the compatibility of protocols and we consider their composition which yields a behaviour protocol for a component assembly. Behaviour protocols are equipped with a model-theoretic semantics which describes the class of all correct component or assembly implementations. Implementation models are again formalised in terms of labelled transition systems and the correctness notion is based on an alternating simulation relation between protocol and implementation which takes into account concrete control and data states. As a major result we show that our approach is compositional, i.e. that locally correct implementation models of compatible protocols compose to a globally correct implementation, thus ensuring independent implementability.