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.