Local Enforceability and Inconsumable Messages in Choreography Models

Abstract

Choreography models describe the communication protocols between services. Every choreography model can be considered either from a global or from a local point of view. The global model specifies a high-level view of the conversation between service components, and can be considered as being interpreted from an observer point of view. The local model is derived from the global model, and specifies the communication-relevant behavior of each component. The connection between global and local models is achieved differently by connecting observing steps with either the send steps or with the receive steps. The consistency of the global model and the local model can be assured by the local enforceability property: any behavior that the local model permits is also possible to observe in the global model. Another important property of choreography models requires the absence of inconsumable messages, i.e., any messages ready to be received may always be received. In this paper, we study the relations between local enforceability and inconsumable messages in case that the local model is obtained from the global model without modification or further constraints. As a part of the conclusions, we show that if a choreography model is free of inconsumable messages, it is also local enforceable no matter how the global model is connected with the local one. This is a desired result because the mechanical checking of inconsumable messages is much more efficient than that of local enforceability. In case of finite state systems one can check the absence of inconsumable messages in a linear time in the size of the local model, whereas checking local enforceability has an exponential complexity.