Database of Case Studies Achieved Using CADP

Collaboration Diagrams

Organisation: University of Málaga (SPAIN)
University of California, Santa Barbara (USA)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Service-Oriented Computing.

Period: 2009

Size: 85 collaboration diagrams
(about 49,000 lines of LOTOS and 23,000 lines of SVL generated)

Description: In service-oriented applications, the choreography describes the interactions among a set of services from a global point of view. Several formalisms have already been proposed to specify choreographies: WS-CDL, collaboration diagrams, process calculi, BPMN, SRML, etc. Given a choreography specification, a desirable feature is to generate peers (i.e., local implementations) automatically via projection. However, generation of peers that precisely implement the choreography specification is not always possible: this problem is known as realizability. So far, no solution has been proposed to generate peers realizing any choreography without adding rules or constraints on the choreography language or on specifications written with it. The contribution of this work is twofold. First, the proposed solution generates peers for any choreography specification by extending them with additional messages if the choreography is unrealizable. Second, the approach is supported by tools for verification of choreographies, testing realizability, and generation of peers in a completely automated way.

Collaboration diagrams are adopted as specification language for choreographies. A collaboration diagram consists of a set of peers, a set of links between peers, and a set of message send events associated with links. To achieve their formal analysis, collaboration diagrams are translated in LOTOS. A collaboration diagram choreography is encoded using a LOTOS process, which is split up in as many parts (thread behaviours) as there are threads in the diagram. Each thread behaviour encodes all the messages involved in its thread in the order in which they must be executed. Each message is encoded using source and target peer names as prefixes to avoid name clashes. The conditional recurrence type is encoded using choice and termination, and the iterative recurrence type is translated into an intermediate looping process. The labelled transition system (LTS) of the resulting LOTOS specification is generated and minimized using the state space manipulation tools of CADP, and verified using the EVALUATOR model checker. Peers are generated by projection from the LOTOS process encoding the collaboration diagram, by generating a LOTOS process for each peer whose body is an instance of the collaboration diagram process, and hiding in this process all the messages in which the peer does not participate in.

Realizability is computed by comparing the collaboration diagram LTS with the system composed of interacting peers using behavioural equivalences. If these two systems are equivalent, it means that the peer generation exactly preserves the collaboration diagram constraints. If they are not, peers do not generate the same interactions than those specified in the diagram, which is therefore unrealizable. Computing realizability is achieved in two steps: (i) generation of the system composed of interacting peers, and (ii) equivalence checking between the LTS resulting from step (i) and the collaboration diagram LTS, using the BISIMULATOR tool of CADP. This is done in both synchronous and bounded asynchronous communication models, all steps being automated using SVL scripts.

To make peers respect interaction constraints of unrealizable collaboration diagrams, additional communications are inserted among peers. Basically, peers have to respect the application order of messages in each thread, and also respect dependency relations which specify constraints on the firing of a specific message. The first constraint is achieved by adding in the collaboration diagram encoding some specific explicit messages between each thread message. Concerning the second constraint, the synchronization messages of the initial encoding are reused to enforce message dependency relations.

Conclusions: This proposal for realizability of choreography specifications allows a completely automated and smooth process thanks to a prototype translator from collaboration diagrams into LOTOS code, and the use of the CADP toolbox to analyze results generated from this code. The peers generated using this approach can be implemented either as new services, or some wrappers can be generated if an implementation of a service already exists. In the latter case, the wrapper aims at constraining the functionality of the existing service to make it respect the application order of operations as specified in the generated peer behaviour. Implementation of executable services (Java, BPEL) from abstract descriptions can be achieved, e.g., using Pi4SOA technologies.

Publications: [Salaun-Bultan-09] Gwen Salaün and Tevfik Bultan. "Realizability of Choreographies Using Process Algebra Encodings". Proceedings of the 7th International Conference on Integrated Formal Methods IFM'09, Lecture Notes in Computer Science vol. 5423, pages 167-182. Springer Verlag, February 2009.
Available on-line at: http://www.cs.ucsb.edu/~bultan/publications/ifm09.pdf
or from the CADP Web site in PDF or PostScript
Contact:
Prof. Tevfik Bultan
Department of Computer Science
University of California
Santa Barbara, CA 93106-5110
USA
Tel: 805 893 4321
Fax: 805 893 8553
Email: [email protected]
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Thu Feb 11 12:22:02 2021.

Back to the CADP case studies page