<  Back to the Polytechnique Montréal portal

Analyse formelle d'orchestrations de services Web

Mohammed Faïçal Abouzaid

PhD thesis (2010)

[img]
Preview
Download (2MB)
Cite this document: Abouzaid, M. F. (2010). Analyse formelle d'orchestrations de services Web (PhD thesis, École Polytechnique de Montréal). Retrieved from https://publications.polymtl.ca/445/
Show abstract Hide abstract

Abstract

RESUME 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.----------ABSTRACT Web Services are emerging technologies and promising for the development, deployment and integration of Internet applications. To provide a richer functionality, Web Services may be composed resulting in a larger service called orchestration. These emerging technologies require the development of tools and techniques that allow to build safe and reliable systems. Existing commercial tools for the design of composed services do not provide means to proceed to formal verication. Therefore, many researches based on various formalisms have been conducted that have given rise to several tools. But, very often, these tools are limited in their scope. However, it is actually admitted that process algebra are appropriate for the specication and analysis of concurrent, reactive, and distributed systems. This thesis presents an original approach to model languages for Web Services compositions and WS-BPEL in particular, that is one of the most popular standard for Web Services orchestrations. We propose a language, called BP-calculus, that is designed around most important WS-BPEL specic features and that aims to be a formal presentation of this standard. The BP-calculus is based on a well-established formalism, the -calculus. By using signicative examples, we show that the BP-calculus is well-suited to the design of complex applications based on Service Oriented Architectures (SOA) including fault or event handlers and instances correlation. We provide all the methods and tools that permit to build and analyze BP-processes : a syntax and a behavioral semantics, a congruence to check compatibility of services and a temporal logic to check desirable behavior of a system by using existing model-checkers. We also present several mappings between these languages : a mapping that allows to translate WS-BPEL processes into BP-processes and then into -calculus, in order to proceed to their formal verication and a mapping from formally veried BP-processes into WS-BPEL processes acting as a generator of WS-BPEL code. A large case study from nancial domain illustrates the relevance and the feasability of our approach. Finally, we present the architecture of a prototype for a general framework dedicated to the verication of existing WS-BPEL processes and the generation of new WSBPEL specications from formal ones.

Open Access document in PolyPublie
Department: Département de génie informatique et génie logiciel
Dissertation/thesis director: John Mullins
Date Deposited: 21 Mar 2011 14:05
Last Modified: 27 Jun 2019 16:49
PolyPublie URL: https://publications.polymtl.ca/445/

Statistics

Total downloads

Downloads per month in the last year

Origin of downloads

Repository Staff Only