Deciding choreography realizability

Since software systems are becoming increasingly more concurrent and distributed, modeling and analysis of interactions among their components is a crucial problem. In several application domains, message-based communication is used as the interaction mechanism, and the communication contract among the components of the system is specified semantically as a state machine. In the service-oriented computing domain such communication contracts are called ”choreography” specifications. A choreography specification identifies allowable ordering of message exchanges in a distributed system. A fundamental question about a choreography specification is determining its realizability, i.e., given a choreography specification, is it possible to build a distributed system that communicates exactly as the choreography specifies? Checking realizability of choreography specifications has been an open problem for several years and it was not known if this was a decidable problem. In this ...

• Type: Journal
• Year: 2012
• Where: POPL
• Authors: Samik Basu, Tevfik Bultan, Meriem Ouederni
• Keywords: Choreographies, Message Exchanges, POPL 2012, Programming Languages, Service Oriented Computing