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...

• Type: Conference
• Year: 2009
• Where: IFM
• Authors: Gwen Salaün, Tevfik Bultan
• Keywords: Choreography Specification, Choreography Specification Languages, Collaboration Diagram, Formal Methods, IFM 2009