Industrial deployment of system engineering methods providing high dependability and productivity


Local Enforceability and Inconsumable Messages in Choreography Models

Kozyura, Vitaly and Roth, Andreas and Wei, Wei (2009) Local Enforceability and Inconsumable Messages in Choreography Models. In: Proceedings of 4th South-East European Workshop on Formal Methods (SEEFM'09).

PDF - Published Version


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.

Item Type:Conference or Workshop Item (Paper)
Subjects:Industrial Deployment > Business
ID Code:190
Deposited By:Dr Andreas Roth
Deposited On:21 Jan 2010 09:21
Last Modified:19 Apr 2010 16:06

Repository Staff Only: item control page

Deploy-Project - All right reserved