Deciding choreography realizability

12 years 3 days ago

Download www.cs.ucsb.edu

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 speciﬁed semantically as a state machine. In the service-oriented computing domain such communication contracts are called ”choreography” speciﬁcations. A choreography speciﬁcation identiﬁes allowable ordering of message exchanges in a distributed system. A fundamental question about a choreography speciﬁcation is determining its realizability, i.e., given a choreography speciﬁcation, is it possible to build a distributed system that communicates exactly as the choreography speciﬁes? Checking realizability of choreography speciﬁcations 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

Real-time Traffic