Database of Research Tools Developed Using CADP

ITACA/ACIDE Toolbox for Composition and Adaptation of Web Services

Organisation: University of Málaga (SPAIN)
INRIA Grenoble

Functionality: Automatic composition and adaptation of Web services.

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

Period: 2009

Description: In today's Web, services are everywhere. These can be just accessed and used to fulfill basic requirements, or be composed with other services to build bigger systems which aim at working out complex tasks. To ease their reuse and enable their automatic composition, services must be equipped with rich interfaces enabling external access to their functionality. Several interoperability levels can be distinguished in interface description languages (i.e., signature, protocol, quality of service, and semantics). Composition of services is seldom achieved seamlessly because mismatch may occur at the different interoperability levels and must be solved. Software adaptation is the only way to compose non-intrusively black-box components or services with mismatching interfaces by automatically generating mediating adaptor services. The so-called generative approaches for software adaptation avoid restricting service behaviour, and support the specification of advanced adaptation scenarios. Generative approaches build adaptors automatically from an abstract specification, namely an adaptation contract, of how mismatch cases can be solved.

ITACA is an integrated toolbox that fully supports generative adaptation, which starts with the automatic extraction of behavioural models from existing interface descriptions either in Abstract BPEL or Windows Workflows (WF). The toolbox enables automatic contract generation, and also interactive contract specification. The latter relies on a graphical notation and a computation of protocol similarity which assists the designer by pointing out parts of service protocols that can be matched together. Interactive specification can be used either as an alternative, or in conjunction with automatic generation. Simulation and verification of the system's execution based on a particular contract before adaptor generation is also possible. Finally, a monolithic adaptor protocol or a set of distributed adaptation wrapper protocols can be automatically generated and deployed.

Service interfaces are assumed to be specified using both a signature and a protocol. Signatures correspond to operation names associated with arguments and return types relative to the messages and data being exchanged when the operation is called. Protocols are represented by means of Symbolic Transition Systems (STSs), which are Labelled Transition Systems (LTSs) extended with value passing. This formal model has been chosen because it is simple, graphical, and provides a good level of abstraction to tackle verification, composition, or adaptation issues. At the user level, one can specify service interfaces (signatures and protocols) using respectively WSDL, and Abstract BPEL (ABPEL) or WF workflows (AWF).

ITACA comprises the following tools:
  • WSDL2SIG parses WSDL descriptions of Web services and generates the corresponding signatures.

  • ABPEL2STS/AWF2STS generates STSs from service interfaces specified using ABPEL or AWF.

  • SIM measures protocol similarity, aiming at pointing out differences between two protocols, but also at detecting parts of them which turn out to be similar.

  • Dinapter aims at generating contracts automatically by traversing the behaviour of the services and matching the operations found based on the metrics returned by SIM.

  • ACIDE aims at helping the designer in specifying a contract by means of a graphical notation enabling interactive and incremental construction, as well as various checks on the contract.

  • (D)Compositor generates LOTOS code for service interfaces, the adaptation contract, and some processes indicating how to obtain distributed wrappers. Beyond simulation and verification techniques integrated in ACIDE, the LOTOS encoding allows to check temporal logic properties on the adaptor under construction using the EVALUATOR model checker of CADP.

  • Scrutator is a tool developed using the OPEN/CAESAR environment of CADP for on-the-fly verification. It returns adaptor and wrapper protocols (STSs) corresponding to the LOTOS specification generated by (D)Compositor, by removing remaining erroneous paths and reducing the STS on-the-fly.

  • STS2BPEL allows the implementation of adaptor models as BPEL orchestrators. It proceeds in two steps: (i) filtering the interleaving cases that cannot be implemented (e.g., several emissions and receptions outgoing from a same state); (ii) encoding the filtered model into the corresponding implementation language. The adaptor protocol is implemented using a state machine pattern, and the main body of the BPEL process corresponds to a global cyclic activity containing branch statements encoding adaptor states. Variables are used to store data passing through the adaptor and the current state of the protocol.

Conclusions: Building systems by adapting a set of reusable software services is an error-prone task which can be supported by assisting developers with automatic procedures and tools. ITACA is the first toolbox that fully supports a generative adaptation approach from beginning to end: specification and verification of adaptation contracts, generation of adaptor protocols, and translation of abstract models in implementation languages.

Publications: [Mateescu-Poizat-Salaun-07] Radu Mateescu, Pascal Poizat, and Gwen Salaün. "Behavioral Adaptation of Component Compositions based on Process Algebra Encodings". Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering ASE'2007 (Atlanta, Georgia, USA), November 2007. Full version available as INRIA Research Report RR-6362.
Available on-line at:
or from our FTP site in PDF or PostScript

[Mateescu-Poizat-Salaun-08] Radu Mateescu, Pascal Poizat, and Gwen Salaün. "Adaptation of Service Protocols using Process Algebra and On-the-Fly Reduction Techniques". Proceedings of the 6th International Conference on Service Oriented Computing ICSOC'2008 (Sydney, Australia), December 1-5, 2008.
Available on-line at:
or from our FTP site in PDF or PostScript

[Camara-Martin-Salaun-et-al-09] Javier Camara, Jose Antonio Martin, Gwen Salaun, Javier Cubo, Meriem Ouederni, Carlos Canal, and Ernesto Pimentel. "ITACA: An Integrated Toolbox for the Automatic Composition and Adaptation of Web Services". Proceedings of the 31st International Conference on Software Engineering ICSE'09, pp. 627-630. IEEE Computer Society Press, May 2009.
Available on-line at:
or from our FTP site in PDF or PostScript

[Camara-Salaun-Canal-Ouederni-09] Javier Camara, Gwen Salaun, Carlos Canal, and Meriem Ouederni. "Interactive Specification and Verification of Behavioural Adaptation Contracts". Proceedings of the 9th International Conference on Quality Software QSIC'2009, pp. 627-630. IEEE Computer Society Press, August 2009.
Available on-line at:
or from our FTP site in PDF or PostScript
Ernesto Pimentel Sánchez
Dpto. de Lenguajes y Ciencias de la Computación
University of Málaga
Campus de Teatinos
29071 Málaga
Tel: +34 95 213 1396
Fax: +34 95 213 1397

Further remarks: This tool, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:13:01 2016.

Back to the CADP research tools page