Verification of Adaptors between Evolving Components

Organisation:	INRIA Paris-Rocquencourt / ARLES (FRANCE) University of Málaga (SPAIN)
Method:	CCS networks of communicating LTSs Petri nets adaptation mappings (regular expressions over synchronization vectors) mu-calculus
Tools used:	ADAPTOR TINA CADP (Construction and Analysis of Distributed Processes)
Domain:	Component-based Systems.
Period:	2007
Size:	n/a
Description:	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.
Conclusions:	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.
Publications:	[Poizat-Salaun-07] 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, June 2007. 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
Contact:	Pascal Poizat Centre de Recherche INRIA Paris-Rocquencourt Equipe-projet ARLES Domaine de Voluceau-Rocquencourt B.P. 105 78153 Le Chesnay Cedex FRANCE Tel: +33 (0)1 39 63 59 69 Email: [email protected]
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page