Deciding choreography realizability

8 years 6 months ago
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 ...
Samik Basu, Tevfik Bultan, Meriem Ouederni
Added 25 Apr 2012
Updated 25 Apr 2012
Type Journal
Year 2012
Where POPL
Authors Samik Basu, Tevfik Bultan, Meriem Ouederni
Comments (0)