Adaptive Service Composition Based on Runtime Verification of Formal Properties

Organisation:	Federal University of Pernambuco (BRASIL) University of Twente (THE NETHERLANDS)
Functionality:	Adaptive Service Composition Based on Runtime Verification of Formal Properties
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2017
Description:	Service-Oriented Computing (SOC) is widely used to smoothly integrate heterogeneous systems in dynamic environments. To cope with the changing requirements, service composition must be flexible, dynamic and adaptive. To ensure correct composition, formal methods have been used. This tool performs formal verification on execution traces, and triggers an adequate reconfiguration plan whenever an undesirable behaviour is detected. The approach has been implemented in Java. The service composition is instrumented to generate an execution trace, which is translated into the SEQ format of CADP. A dedicated checker component then invokes the SEQ.OPEN and EVALUATOR tools to check several properties on the trace, such as the absence of deadlocks, and requirements on the order in which actions appear. The properties are specified in the regular alternation-free μ-calculus using Dwyers' patterns. Experiments have shown that although the approach induces some overhead (monitoring the service composition, formally checking undesirable behaviour, and devising a reconfiguration plan), the service composition adaptation is better than its execution producing undesirable behaviors.
Conclusions:	The authors motivate the choice of CADP as follows: "By using CADP Toolbox, we can choose to check different properties by trace file, such as deadlocks, temporal formulas, generating tests and evaluating performance."
Publications:	[Campos-Rosa-Pires-17] Glaucia M. M. Campos, Nelson Souto Rosa, and Luis Ferreira Pires. "Adaptive Service Composition Based on Runtime Verification of Formal Properties". Proceedings of the 50th Hawaii International Conference on System Sciences (HICSS 2017), Hilton Waikoloa Village, Hawaii, USA, AIS Electronic Library (AISeL), January 2017. Available on-line at: http://aisel.aisnet.org/hicss-50/os/enterprise_architecture/5 or from the CADP Web site in PDF or PostScript
Contact:	Glaucia M. M. Campos Federal University of Pernambuco Center of Informatics Recife, Brazil Email: gmmc@cin.ufpe.br
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page