A Tool for Choreography Analysis Using Collaboration Diagrams

Analyzing interactions among peers that interact via messages is a crucial problem due to increasingly distributed nature of current software systems, especially the ones built using the service oriented computing paradigm. In service oriented computing, interactions among peers participating to a composite service involve message exchanges across organizational boundaries in a distributed computing environment. In order to build such systems in a reliable manner, it is necessary to develop techniques for analysis and verification of interactions among services. Collaboration diagrams provide a convenient visual model for modeling service interactions. In this paper, we present a tool that (1) checks the realizability of interactions specified by the given collaboration diagram, (2) verifies the LTL properties of the interactions specified by the given collaboration diagram by automatically converting it to a state machine model, and (3) synthesizes peer state machines that realize the set of interactions specified by the given collaboration diagram.