University of Málaga (SPAIN)
University of California, Santa Barbara (USA)
CADP (Construction and Analysis of Distributed Processes)
85 collaboration diagrams
(about 49,000 lines of LOTOS and 23,000 lines of SVL generated)
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.
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
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
Prof. Tevfik Bultan
Department of Computer Science
University of California
Santa Barbara, CA 93106-5110
Tel: 805 893 4321
Fax: 805 893 8553
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|