Sebastian Bauer : Behaviour Protocols for Interacting Stateful Components with Ports

Joint work with Rolf Hennicker and Stephan Janisch

 

Abstract:

 

We propose a formal foundation for behaviour protocols of interacting components with (encapsulated) 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 control and data states. As a major result we show that our approach is compositional, i.e. that correct implementation models of compatible protocols compose to a correct implementation of the resulting assembly protocol.