Analyse formelle d'orchestrations de services Web

Les Services Web sont des technologies émergentes et prometteuses pour le développement, le déploiement et l'intégration des applications Internet. Plusieurs Services Web sont composés pour fournir des fonctionnalités plus riches donnant naissance à ce qu'il est convenu d'appeler une orchestration de services. Ces nouvelles technologies nécessitent l'élaboration d'outils et de techniques permettant la conception de systèmes plus sûrs et plus fiables. Les outils commerciaux existants de conception de compositions de services ne fournissent pas de fonctionnalités pour la vérication formelle. Par conséquent, plusieurs recherches basées sur des formalismes variés ont été menées donnant lieu a la réalisation de nombreux outils dédiés à la vérication de Services Web. Mais, très souvent, ces outils sont limites dans leur portée. Ceci nous a amenés à privilégier l'utilisation des algèbres de processus qui sont généralement admis comme étant un formalisme plus adapté à la spécification et à l'analyse des systèmes concurrents distribués ee réactifs. Cette thèse présente une approche originale pour la modélisation de langages de compositions de Services Web et du langage WS-BPEL en particulier. Ce langage est l'un des standards les plus populaires pour les orchestrations de Services Web. Nous proposons ainsi un formalisme que nous appelons le BP-calcul et qui est conçu autour des caractéristiques les plus importantes de WS-BPEL. Le BP-calcul vise à ^êre une représentation formelle de ce standard. Il est basé sur un formalisme bien établi, le -calcul. En utilisant des exemples significatifs, nous montrons que le BP-calcul est adapté à la conception d'applications complexes basées sur les services qui peuvent contenir tout autant des gestionnaires d'erreurs ou d'événements que des mécanismes de corrélation d'instances. Nous fournissons toutes les méthodes et les outils qui permettent de construire et d'analyser des BP-processus. Nous fournissons ainsi une syntaxe et une sémantique comportementale, une congruence permettant de vérifier la compatibilité entre services ainsi qu'une logique temporelle permettant de vérifier les comportements souhaitables d'un système à l'aide de model-checkers existants. Nous présentons également différentes transformations entre ces trois langages. Une première transformation permet de traduire les processus WS-BPEL en BP-processus, puis ensuite en -calcul, ce qui permet leur vérication formelle. Une autre transformation traduit des BP-processus formellement vérifiés en processus WS-BPEL, agissant ainsi comme un générateur de code WS-BPEL. Nous démontrons de nombreux théorèmes qui attestent du bien fondé de ces transformations. Une étude de cas conséquente dans le domaine financier illustre la pertinence et la faisabilité de de notre approche. Enfin, nous présentons l'architecture du prototype d'un environnement dédié à la vérification des processus WS-BPEL existants et la création de nouveaux processus WS-BPEL à partir de spécifications formelles conçues en BP-calcul.