INRIA Paris-Rocquencourt / ARLES (FRANCE)
University of Málaga (SPAIN)
networks of communicating LTSs
adaptation mappings (regular expressions over synchronization vectors)
CADP (Construction and Analysis of Distributed Processes)
Software adaptation aims at facilitating reuse by generating software
pieces called adaptors to compensate interface and behavioural
mismatch between components or services. So far, adaptation techniques
have proceeded by computing global adaptors for closed systems made up
of a fixed set of components. This is not satisfactory when the systems
may evolve, with components entering or leaving at any time, e.g.,
for pervasive computing. To enable adaptation on such systems, the
authors propose new techniques and automated tools for building
adaptors for open systems in an incremental way.
Components are described by means of their signatures and behavioural interfaces, which are subsequently translated into LTSs according to standard process algebra semantics. The interaction between components is specified using synchronization vectors and the semantics of open component systems is given by a notion of open synchronous product applied hierarchically on sets of LTSs. Adaptation mappings are defined as regular expressions over an alphabet of synchronization vectors.
The adaptor generation approach for open systems works by translating adaptation constraints (mirroring of behavioural interfaces, adaptation mapping) into a Petri net whose marking graph is generated using TINA (modulo appropriate abstractions if necessary) and reduced modulo branching bisimulation using the BCG_MIN tool of CADP, yielding the LTS of the adaptor. This technique is further extended to deal with the addition and suppression of components, allowing to generate adaptors for evolving systems. The behaviour of the resulting adapted systems can be further assessed w.r.t. correctness criteria using model checking and equivalence checking tools.
The adaptation method proposed is illustrated on a library management system. It consists of three components, in charge of testing the availability of books in the library, checking whether a user is a subscriber of the library, and handling loan requests, respectively. The adaptors for each component were generated automatically and the resulting adapted system was checked to be deadlock-free and to satisfy a liveness property using the EVALUATOR tool of CADP.
The proposed adaptation approach allows to deal with open and evolving
component systems, by computing adaptors incrementally. Moreover, the
formal framework used (process algebras and LTSs, synchronization
vectors, open synchronous products, adaptation mappings) benefits
from all the construction, reduction, and analysis functionalities
of the verification tools available for concurrent systems.
Pascal Poizat and Gwen Salaün.
"Adaptation of Open Component-based Systems."
In Proceedings of the IFIP International Conference on Formal
Methods for Open Object-Based Distributed Systems FMOODS'2007
(Paphos, Cyprus), LNCS vol. 4468, pp. 141-156. Springer Verlag,
Available on-line from http://www.ibisc.univ-evry.fr/~poizat/documents/publications/PS07.pdf
or from the CADP Web site in PDF or PostScript
Centre de Recherche INRIA Paris-Rocquencourt
Domaine de Voluceau-Rocquencourt
78153 Le Chesnay Cedex
Tel: +33 (0)1 39 63 59 69
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies