Return to search

Vérification de processus BPEL à l'aide de promela-spin

L'objectif de notre travail de recherche est de vérifier si un processus BPEL satisfait sa spécification d'interface représentant son comportement externe en utilisant la vérification de modèles. Dans ce mémoire, nous présentons essentiellement l'approche de notre logiciel qui permet dans un premier temps de traduire un processus BPEL en modèle Promela et une expression d'interface en assertion de traces, et par la suite, il lance la vérification en utilisant l'outil Spin. Cette vérification du comportement du processus concret se fait par rapport à une spécification abstraite de son interface comportementale, c'est-à-dire, nous vérifions uniquement ce qui est visible à l'exterieur du processus. Nous expliquons les étapes franchies pour atteindre notre objectif et nous montrons à l'aide d'exemples que notre logiciel est fonctionnel.

Identiferoai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QMUQ.1398
Date January 2008
CreatorsChami, Aida
Source SetsLibrary and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada
Detected LanguageFrench
TypeMémoire accepté, PeerReviewed
Formatapplication/pdf
Relationhttp://www.archipel.uqam.ca/1398/

Page generated in 0.0017 seconds