Vérification de modèle de processus métier.

Abstract

La vérification de modèle de processus métier est basée sur des techniques formelles nécessitant en entrée un modèle qui formalise le processus. Un modèle de processus métier consiste en un ensemble de modèles d'activités et de contraintes d'exécution. Ce dernier fera par la suite l'objet d'une vérification. Dans ce cadre, notre procédure de modélisation consiste à transformer les modèles de processus métier, décrit en BPMN, en réseaux de Petri. Le modèle résultant de l'étape de modélisation consiste en un graphe (réseau de Petri) qui exprime le comportement global du système. Evidemment, les représentations graphiques constituent des spécifications semi-formelles. Or, les techniques de vérification reposent sur le besoin d'une spécification formelle en entrée. Partant du principe que nous avons, comme donnée, une spécification formelle qui exprime le réseau de Petri représentant le système à vérifier, notre travail consiste à appliquer des techniques de traitement automatique afin d'extraire les données nécessaires du réseau et les exploiter. Et ce, en respectant le principe général de la méthode du model-checking qui prend en entrée la spécification formelle ainsi que les propriétés comportementales du réseau que l'on souhaite vérifier. Ainsi, en explorant exhaustivement l'ensemble des états du système, elle fournit les résultats de la vérification plus les contre-exemples dans le cas où la propriété en question est violée. Mots-clefs : BPMN, RdP, model-checking, PM, modèle de processus métier, vérification de processus métier, processus collaboratif.