Architecture Orientée Service et Services Web / Architecture du système de l’agence du voyage /Labelled Transition System

Abstract

Dans ce travail, une spécification d’un système de réservation de voyage basé sur la composition des services Web a été élaborée. Nous avons opté pour l’algèbre de processus qui est muni d’une expressivité permettant la spécification du comportement de systèmes en les disséquant en leurs composants concurrents. Ce formalisme offre le moyen de spécifier des systèmes complexes de manière précise et relativement concise. Nous avons utiliser le langage LOTOS, un langage de description formelle standardisé par l’ISO, car il offre, en plus de son expressivité puissante en terme d’opérateurs, le moyen de représenter les données en utilisant les types abstraits de données (TADs). Nous avons également étudié l’outil de «CADP», développé spécialement par l’équipe VASY1 de l’Inria Rhones–Alpes pour le langage LOTOS. Cet outil nous a permis de compiler notre spécification et de vérifier certaines propriétés telles que : la sureté, la atteignabilité. En effet, L’étape de vérification est indispensable à toute approche moderne de développement logiciel. Il est nécessaire de vérifier et tester tout nouveau système logiciel avant sa mise en commercialisation et son utilisation. L’étape de vérification permet non seulement d’assurer la fiabilité mais contribue également à limiter les coûts puisque la découverte d’erreurs de conception après la mise en production d’un système peut engendrer des coûts importants. les outils de vérification formelle procèdent à une compilation du modèle vérifié afin d’obtenir une représentation mathématique. L’outil est alors en mesure d’explorer de manière exhaustive toutes les branches d’exécution possibles sur la représentation mathématique. Notre tâche se résume alors à définir des propriétés comportementales à l’aide de la logique temporelle et ces propriétés seront vérifiées de manière exhaustive et automatique par l’outil. Ainsi, notre travail nous a permis d’apprendre et d’expérimenter la spécification dans le langage LOTOS, ainsi que l’utilisation de l’outil CADP pour la vérification d’un système de réservation de voyage, basé sur la composition des services Web. Nous nous sommes intéressés dans ce travail à la composition des services Web par orchestration. Il s’agit d’une approche centralisée où les clients interagissent avec un service composé central au lieu d’interroger directement les services atomiques existants. Il serait intéressant de spécifier et vérifier dans un travail futur un système basé sur la composition de services en utilisant la chorégraphie. La chorégraphie de services est une alternative distribuée à l’orchestration qui consiste à concevoir une coordination décentralisée des applications.