Verification of a .Net On-Line Sale Application

Organisation:	University of Málaga (SPAIN) INRIA Paris-Rocquencourt / ARLES (FRANCE)
Method:	networks of communicating LTSs synchronization vectors mu-calculus
Tools used:	ADAPTOR CADP (Construction and Analysis of Distributed Processes)
Domain:	E-commerce.
Period:	2007
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 in order to fit specific needs within different systems. In such a way, application development is mainly concerned with the selection, adaptation and composition of different pieces of software rather than with the programming of applications from scratch. Many approaches dedicated to model-based adaptation focus on the behavioural interoperability level and aim at generating new components, called adaptors, responsible for solving mismatch in a non-intrusive way. This process is completely automated being given an adaptation mapping, which is an abstract description of how mismatch can be solved with respect to the behavioural interfaces of components. The authors focus on Windows Workflow Foundation (WF) which belongs to the .NET Framework 3.0 developed by Microsoft. This platform supports the behavioural descriptions of components/services using workflows. In addition, the .NET Framework is widely used in private companies, and makes the implementation of services easier thanks to its workflow-based graphical support and the automation of the code generation. Besides adaptation of WF components, the approach also allows the verification of such components by extracting abstract descriptions from them and by using model-checking tools. The proposed adaptation approach consists of the following 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, an adaptor protocol/LTS is generated automatically from a mapping using adaptation techniques. The adaptor produced is then formally verified in order to ensure that it behaves as expected. If not, another mapping may be proposed and the whole process is repeated until a suitable adaptor is obtained. Formal verification of WF components takes place twice: when detecting mismatch and when assessing the resulting system (components+adaptor). Last, once the designer is satisfied by the abstract adaptor, the corresponding WF workflow is generated. This approach is illustrated by the construction and verification of an on-line computer sale system, whose purpose is to sell computer material such as PCs, laptops, or PDAs to clients. The system is built by adapting two existing components, a buyer and a supplier, both implemented using WF./NET. The LTSs modeling the behaviour of the components are extracted from their WF workflows and their composition is checked for mismatches. Three types of mismatches are identified, regarding the conflicting names of messages to be exchanged, the different number of messages, and the independent evolution of components. These mismatches are solved by means of an adaptation mapping given as a set of synchronization vectors. Then, the adaptor protocol is generated using the ADAPTOR tool and three liveness properties are checked on the whole system (made of the two components and the adaptor) using the EVALUATOR model checker of CADP. Finally, the WF description of the adaptor has been generated from the abstract LTS obtained. The whole system was thus completely implemented using WF and the buyer and supplier components worked as required thanks to the use of the adaptor component.
Conclusions:	The model-based approach for software adaptation allows to exploit the existing verification and LTS manipulation tools for automating the detection of mismatches, the generation of adaptors, and the assessment of the adapted system. Software adaptation can be of real interest for widely used implementation platforms such as the .NET Framework 3.0, and 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. "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'07 (Sophia-Antipolis, France), September 2007. To appear in Electronic Notes in Theoretical Computer Science (ENTCS). Available on-line from http://www.ibisc.univ-evry.fr/~poizat/documents/publications/CSCPP08.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: Pascal.Poizat@inria.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