Modeling and functional testing of Web services orchestrations

Ces dernières années ont vu l’émergence d’architectures orientées services (SOA) conçues pour faciliter la création, l’exposition, l’interconnexion et la réutilisation d’applications à base de services. Les services Web sont la réalisation la plus importante de cette architecture SOA. Ce sont des applications auto descriptives et modulaires fournissant un modèle simple de programmation et de déploiement d’applications. La composition de services Web, en particulier l’orchestration, est au coeur de l’ingénierie à base de services (SOC pour Service Oriented Computing) puisque elle supporte la construction de nouveaux services composés à partir de services de base. De son côté, WS-BPEL (ou BPEL) s’est imposé depuis 2005 comme le langage standard d’orchestration de services Web. Cette thèse de Doctorat s’articule autour du test fonctionnel de l’orchestration de services décrite en langage BPEL, qui consiste à établir la conformité de l’implantation d’un service composé par rapport à sa spécification. Nos activités de recherche ont été motivées par les caractéristiques spécifiques de la composition de services surtout celle décrite en BPEL, et par la nécessité d’automatisation des tests. L’objectif de cette thèse est double : d’une part, proposer une modélisation formelle de l’orchestration de services, et d’autre part, proposer une méthode de test complète de l’orchestration de services, allant de la modélisation formelle de l’orchestration à l’exécution des tests, incluant la génération automatique de cas de test. Notre modèle formel (appelé WS-TEFSM) permet de décrire une grande partie de BPEL et prend en considération les propriétés temporelles de la composition de service. La modélisation formelle est la première phase de notre approche de test. Par conséquent, nous utilisons le modèle formel résultant pour la génération de cas de test satisfaisant un ensemble d’objectifs de test. L’automatisation de la génération de cas de test a été mise en oeuvre par l’implémentation d’une stratégie efficace d’exploration partielle de l’espace d’états (i.e. Hit-Or-Jump) dans le simulateur IF. Pour se focaliser seulement sur les erreurs potentielles du service orchestrateur (service composé), nous proposons une approche de test boîte grise consistant à simuler les services partenaires de cet orchestrateur. Nous avons abordé ces problématiques à la fois d’un point de vue théorique et pratique. En plus de la proposition d’une modélisation formelle de l’orchestration de services et d’un algorithme de génération de cas de test temporisés, nous avons implémenté ces deux concepts en développant deux prototypes. BPEL2IF permet de transformer une orchestration de services décrite en BPEL en une spécification formelle à base d’automates temporisés (spécification IF). TestGen-IF permet de dériver automatiquement des cas de test temporisés. Enfin, pour valider notre démarche, nous avons appliqué notre approche de test à des cas d’études de taille réelle.Last years have seen the emergence of the service oriented architecture (SOA) designed to facilitate the creation, the publication, the networking and the reuse of applications based on services. Web services are the most important realization of the SOA architecture. They are self descriptive and modular entities which provide a simple model of programming and application deployment. Web services composition, especially orchestration, is at the heart of service oriented computing (SOC), since it supports the construction of new composite services out of basic services. WS-BPEL (BPEL for short) has emerged since 2005 as the standard language for Web service orchestration. This PhD thesis focuses on functional testing of service orchestrations described in BPEL, which aims to establish the conformance of a composite service implementation to its specification. Our research activities have been motivated by specific features of the BPEL composition, and the need for test automation. The objective of this thesis is twofold : on the one hand, to propose a formal modeling of service orchestration, and on the other hand, to propose a comprehensive testing approach for orchestrations, ranging from orchestration modeling to tests execution, including automatic test case generation. Compared to existing work, our formal model covers a large subset of BPEL constructs and focuses on the temporal properties of the composition. The formal model is a first step of our testing approach. Afterwards, we use the model to generate the test cases according to test purposes. We automate the test generation by implementing an efficient state space search strategy inside an open-source simulator, i.e. the IF simulator. In our case, to focus on the potential errors of the orchestrator, we propose a gray box approach which consists on the simulation of the partners of this orchestrator. We have addressed these issues both from a theoretical and practical perspective. Therefore, besides proposing expressive orchestration models and test case generation algorithm, we have developed prototypes (BPEL2IF and TestGen-IF) as a proof of concepts. BPEL2IF transforms a BPEL orchestration into a formal specification based on timed automata (IF specification). TestGen- IF generates automatically timed test cases. Moreover, to validate our proposal, we have applied our testing approach on real size case studies