Federal University of Pernambuco (BRASIL)
University of Twente (THE NETHERLANDS)
Adaptive Service Composition Based on Runtime Verification of Formal Properties
CADP (Construction and Analysis of Distributed Processes)
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.
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
Glaucia M. M. Campos, Nelson Souto Rosa, and Luis Ferreira Pires.
"Adaptive Service Composition Based on Runtime Verification of Formal
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 our FTP site in PDF or PostScript
Glaucia M. M. Campos
Federal University of Pernambuco
Center of Informatics
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|