A Tool for Choreography Analysis Using …

1 A Tool for Choreography Analysis Using Collaboration DiagramsTevfik BultanChris FergusonUniversity of California Santa FuHofstra interactions among peers that interact viamessages is a crucial problem due to increasingly dis-tributed nature of current software systems, especially theones built Using the service oriented computing service oriented computing, interactions among peersparticipating to a composite service involve message ex-changes across organizational boundaries in a distributedcomputing environment. In order to build such systems in areliable manner, it is necessary to develop techniques foranalysis and verification of interactions among diagrams provide a convenient visual modelfor modeling service interactions. In this paper, we presenta tool that 1) checks the realizability of interactions speci-fied by the given collaboration diagram, 2) verifies the LTLproperties of the interactions specified by the given collab-oration diagram by automatically converting it to a statemachine model, and 3) synthesizes peer state machines thatrealize the set of interactions specified by the given collab-oration IntroductionService oriented computing provides technologies thatenable multiple organizations to integrate their businessesover the Internet.

2 Typical execution behavior in such a dis-tributed system involves a set of autonomous peers inter-acting with each other through messages. Choreographyspecification languages, such as the Web Services Choreog-raphy Description Language (WS-CDL), are used for spec-ification of such interactions. A Choreography specificationidentifies the global ordering of the messages exchangedamong the peers participating to a composite service. Wecall such message sequences conversations, , a choreog-raphy specification identifies the set of allowable conversa-tions for a composite web diagrams (called communication dia-grams in [20]) provide a convenient visual formalism forspecifying the Choreography among the services (peers)participating to a composite service [6]. Characterization ofRealizabilityAnalyzerDependencyGraphCo nstructorAutomataConstructorConversation ProtocolTranslatorCollaborationDiagramsR ealizabilityAnalysiswith WSATP romelaTranslatorLTL Model Checkingwith SPINPeerSynthesizerFigure tool for Choreography analysisinteractions Using a global view, as collaboration diagramsallow us to do, can lead to specification of choreographiesthat may not be implementable.

3 Hence, Using collaborationdiagrams for Choreography specification leads to the follow-ing realizability problem: Given a Choreography specifica-tion, is it possible to find a set of distributed peers which in-teract exactly according to the Choreography a collaboration diagram is realizable, then we can checkthe properties of the interactions among the peers by inves-tigating the possible message orderings allowed by the col-laboration this paper we present a toolset for verification andanalysis of choreographies specified Using collaboration di-agrams. As shown in Figure 1, our tool consists of sixcomponents: The first component constructs a dependencygraph for the events in the input collaboration diagram. Thesecond component checks the realizability of the input col-laboration diagram by checking a set of conditions on thisdependency graph.

4 The third component converts the col-laboration diagram to a finite state automaton such that thelanguage accepted by the automaton is equal to the set of in-teractions specified by the input collaboration diagram. Thefourth components converts the collaboration diagram au-tomaton to the input language of the Web Service AnalysisTool (WSAT) [11] (a tool developed for checking realiz-ability web service Choreography specifications) to checka different set of realizability conditions. The fifth com-ponent converts the collaboration diagram automaton to aPromela specification in order to check LTL properties us-ing the Spin model checker [13]. Finally, the sixth compo-1nent synthesizes a set of state machines that generate ex-actly the set of interactions specified by the collaborationdiagram automaton. We collected a set of collaborationdiagrams from the literature and analyzed them Using thistoolset.

5 Our experiments indicate that realizability Analysis ,LTL model checking and synthesis for collaboration dia-grams is very efficient and can easily be used in contributions in this paper can be summarized asfollows: 1) Extending the semantics for a single collabo-ration diagram given in [6] to collaboration diagram setsand graphs, with increasing expressive power. 2) An algo-rithm for converting collaboration diagrams/sets/graphstoan automaton that accepts the same set of conversations. 3)A translator for converting the collaboration diagram au-tomaton to a Promela model, enabling LTL model checkingusing the Spin model checker [13]. 4) Implementing the re-alizability check for single collaboration diagrams from [6].5) A translator for converting the collaboration diagram au-tomaton to a Conversation Protocol, enabling realizabilitycheck for collaboration diagram sets/graphs Using the re-alizability Analysis for conversation protocols implementedin Web Service Analysis Tool [11].

6 6) A peer synthe-sis algorithm for generating state machine implementationsfor peers for realizable collaboration diagrams/sets/graphsby projecting the collaboration diagram automaton to eachpeer participating to the collaboration. 7) Experiments withseveral collaboration diagrams from the WorkMessage Sequence Charts (MSCs) pro-vide another visual model for specification of interactionsin distributed systems. MSC model has also been used inmodeling and verification of web services [8]. However,collaboration diagrams provide a global view of interactionswhere as MSCs provide a local view. The realizability prob-lem for MSCs [2] have been studied before. However as wementioned above, the type of interactions specified by col-laboration diagrams and MSCs are has been work on formalizing Choreography spec-ifications Using process algebras [7, 16].

7 Our work is com-plementary to work on formalizing semantics of choreog-raphy specification languages. Our focus in this paper isformal visual representations that can be used by servicedevelopers to visualize their has been earlier work on Using various UML dia-grams in modeling different aspects of service compositions(for example [3, 18]). Specification and Analysis of webservice interactions Using conversation protocols has beeninvestigated [10, 12]. In this paper, we investigate the rela-tionship between the collaboration diagrams and the conver-sation protocols Using the collaboration diagram semanticsfrom [6]. A complementary approach to the one presentedhere is discussed in [17], where realizability of collabora-tion diagrams is analyzed Using process algebra , compared to these earlier works, in this paper weextend the collaboration diagram semantics to collaborationdiagrams sets and collaboration diagram graphs which havemore expressive Formal ModelWe assume that a Choreography specification consists ofa finite set of peersP, and a finite set of messagesM.

8 Eachmessagem Mhas a unique sender and a unique receiverdenoted bysend(m) Pandrecv(m) P, that, messages can always be converted to this formby concatenating each message with tags its sender and is a sequence of messages exchangedamong the peers that participate to a composite web service, , M . AchoreographyCis a set of conversations, ,C M .scheduler:FactorySchedulermanager:Facto ryJobManageroven:Ovenrobot:Robot1: start1/B1:startRobotB2:completedRobot1/A 1:startOvenA2:completedOvenA2,B2/2:compl eted1:start1/A1:startOvenA2:completedOve n1/B1:startRobotB2:completedRobotA2,B2/2 :completedFigure collaboration diagram (top) and its depen-dency relation (bottom)Figure 2 shows an example collaboration diagram fromthe UML diagram consists of fourpeers Scheduler, Manager, Oven, Robot. The edges thatconnect the boxes shows the links between the peers.

9 A linkbetween two peers indicate that they can send each othermessages. In collaboration diagrams, message send eventsare shown as arrows drawn over the links. The direction ofthe arrow indicates the sender and the receiver (the arrowpoints to the receiver). Each send event is marked with asequence label. The sequence labels specify the ordering ofthe message send ,acollaborationdiagramC=(P, L, M, E, D)consists of a set of peersP, a set oflinksL P P, a set of messagesM, a set of message2send eventsEand a dependency relationD E Eamong the message send events [6]. For each messagem M, the sender and the receiver ofmmust be linked, ,(send(m),recv(m)) a collaboration diagram, each message send event hasa unique sequence label. Each sequence label consists of apossibly empty prefix followed by a sequence number. Thenumeric ordering of the sequence numbers defines an im-plicit total ordering among the message send events withthe same prefix.

10 Each prefix represents amessage threadwhere each message thread refers to a set of messages thathave a total ordering and that can be interleaved arbitrarilywith other messages. For example, event A2 can occur onlyafter the event A1, but B1 and A2 do not have any implicitordering. In addition to the implicit ordering defined by thesequence numbers, it is possible to explicitly state the eventsthat should precede an eventeby listing their sequence la-bels (followed by the symbol / ) before the sequence labelof the evente. For example if an eventeis marked with B2,C3/A2 then A2 is the sequence label of the evente,and the events with sequence labels B2, C3 and A1 mustprecedee. Also, message send events can be marked to beconditional, denoted as a suffix [condition] , or iterative,denoted as a suffix *[condition] , whereconditionis writ-ten in some , the set of send eventsEis a set of tuples of theform(l, m, r)wherelis the label of the event,m Misa message, andr {1,?}