Verification and Adaptation of WF/.NET Components

Organisation:	Department of Computer Science, University of Málaga (SPAIN) INRIA/ARLES Project-Team (FRANCE) IBISC FRE 2873 CNRS - Université d'Évry (FRANCE)
Method:	Labelled Transition Systems and synchronization vectors
Tools used:	CADP (Construction and Analysis of Distributed Processes) WF (Windows Workflow Foundation)
Domain:	Software Adaptation.
Period:	2007-2008
Size:	n/a
Description:	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 adaptation capabilities. 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.
Conclusions:	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.
Publications:	[Cubo-Salaun-Canal-Pimentel-Poizat-07] 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
Contact:	Pascal Poizat LRI, Bâtiment 490 Université Paris-Sud 11 91405 Orsay Cedex, France Tel: (+33) 1 72 92 59 62 Email: Pascal.Poizat@lri.fr
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