Realizability of Choreographies Using Process Algebra Encodings

8 years 10 months ago
Realizability of Choreographies Using Process Algebra Encodings
Abstract. Service-oriented computing has emerged as a new programming paradigm that aims at implementing software applications which can be used through a network via the exchange of messages. Interactions among a set of services involved in a new system are described from a global point of view using choreography specification languages such as WS-CDL or collaboration diagrams. In this paper, we present an encoding of collaboration diagrams into the LOTOS process algebra. This encoding allows to (i) check choreography specification using the LOTOS verification toolbox (CADP), (ii) check realizability of collaboration diagrams for both synchronous communication and bounded asynchronous communication, and (iii) automate service peer generation. Realizability indicates whether peers can be generated from a choreography such that they will behave exactly as formalized in its specification. If the collaboration diagram is unrealizable, our approach extends the peer generation process b...
Gwen Salaün, Tevfik Bultan
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where IFM
Authors Gwen Salaün, Tevfik Bultan
Comments (0)