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

Chami, Aida (2008). « Vérification de processus BPEL à l'aide de promela-spin » Mémoire. Montréal (Québec, Canada), Université du Québec à Montréal, Maîtrise en informatique.

Fichier(s) associé(s) à ce document :

Prévisualisation	PDF Télécharger (2MB)

Résumé

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.

Type:	Mémoire accepté
Informations complémentaires:	Le mémoire a été numérisé tel que transmis par l'auteur.
Directeur de thèse:	Tremblay, Guy
Mots-clés ou Sujets:	SPIN (Logiciel), Model-checking (Informatique), Processus logiciel, Processus d'affaires, Service Web
Unité d'appartenance:	Faculté des sciences > Département d'informatique
Déposé par:	RB Service des bibliothèques
Date de dépôt:	27 nov. 2008
Dernière modification:	01 nov. 2014 02:07
Adresse URL :	http://archipel.uqam.ca/id/eprint/1398

Modifier les métadonnées (propriétaire du document)

Statistiques