Department of Computer Science, University of Málaga (SPAIN)
INRIA/ARLES Project-Team (FRANCE)
IBISC FRE 2873 CNRS - Université d'Évry (FRANCE)
Labelled Transition Systems and synchronization vectors
CADP (Construction and Analysis of Distributed Processes)
WF (Windows Workflow Foundation)
Software adaptation is a promising research area which aims at
supporting the building of component systems by reusing software
entities. These can be adapted to fit specific needs within different
systems, thus allowing the application development to concentrate on
the selection, adaptation, and composition of different pieces of
software rather than with the programming of applications from scratch.
Many approaches for software adaptation work by generating new
components called adaptors, which are used to solve mismatches
in a non-intrusive way. This process is completely automated given an
adaptation mapping, which is an abstract description of how
mismatches can be solved with respect to the behavioural interfaces of
components. This work focuses on enhancing the WF/.NET framework with
The WF platform supports the behavioural descriptions of components and services using workflows. The adaptation approach proposed for WF consists of several steps. First, abstract behavioural descriptions (Labelled Transition Systems, LTSs) are extracted from WF workflows. Next, being given a set of LTSs, mismatch detection is computed to check whether the involved components need adaptation or not. If a mismatch exists, automatic adaptation techniques are applied in order to produce an adaptor protocol/LTS from a mapping. Assessment techniques are helpful to check that the adaptor is as expected and, if this is not the case, another mapping may be proposed. Last, once the designer is satisfied by the abstract adaptor, the corresponding WF workflow is generated.
The approach is illustrated by means of an on-line computer sale system, which is built from two existing buyer and supplier components. Once the LTSs modelling the behaviour of these components were extracted from their WF descriptions, the detection of mismatches is performed using CADP by generating the LTS corresponding to the parallel composition with full synchronization of these LTSs. An adaptation mapping is provided as a set of synchronization vectors, which solves the mismatches related to naming, correspondence of actions, and independent evolution of components. Given this mapping, the LTS of the adaptor protocol is generated automatically and then composed with the two original buyer and supplier processes. Several correctness properties are checked on the resulting system using the EVALUATOR model checker of CADP: a supplier always replies to a buyer request; a buyer request is always followed by a stop, purchase, or request; and a buyer request is always followed by stop or purchase. Finally, the adaptor LTS is transformed into an abstract workflow, which is subsequently refined into a WF workflow. The resulting on-line sale system works as required thanks to the use of the adaptor component driving the interaction between the buyer and supplier components.
The approach proposed allows to formally verify WF components and, in
case they cannot be directly composed, to generate an adaptor protocol
encoded as a new WF component in charge of solving mismatches. Formal
verification using CADP takes place twice during the adaptation
process, namely when detecting mismatches and when assessing the
resulting system involving the components and the adaptor. This work
is promising because it demonstrates that software adaptation can be
of real interest for widely used implementation platforms such as
the .NET framework, an can help the developer in building software
applications by reusing software components or services.
Javier Cubo, Gwen Salaün, Carlos Canal, Ernesto Pimentel, and
Pascal Poizat. "Relating Model-Based Adaptation and Implementation
Platforms: A Case Study with WF/.NET 3.0". In Ralf Reussner, Clemens
Szyperski, and Wolfgang Weck, editors, Proceedings of the 12th
International Workshop on Component-Oriented Programming WCOP'2007
(Berlin, Germany), pages 9-13, July 2007.
Full version available on-line at: http://www.lri.fr/~poizat/documents/publications/CSCPP07.pdf
or from the CADP Web site in PDF or PostScript
[Cubo-Salaun-Canal-Pimentel-Poizat-08] Javier Cubo, Gwen Salaün, Carlos Canal, Ernesto Pimentel, and Pascal Poizat. " A Model-Based Approach to the Verification and Adaptation of WF/.NET Components". In Proceedings of the 4th International Workshop on Formal Aspects of Component Software (FACS 2007) Sophia-Antipolis, France, pp. 39-55, Elsevier, June 2008.
Available on line at: http://www.lri.fr/~poizat/documents/publications/CSCPP08.pdf
or from the CADP Web site in PDF or PostScript
LRI, Bâtiment 490
Université Paris-Sud 11
91405 Orsay Cedex, France
Tel: (+33) 1 72 92 59 62
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies