La vérification formelle de diagrammes UML

Abstract

La technologie de workflow, tendant à automatiser les processus métier et à fournir un support pour leur gestion. Cependant l’exactitude de leur modélisation influe sur la performance de l’entreprise. Dans ce mémoire, nous allons utiliser les diagrammes d’activités de langage UML pour modéliser ces processus workflow. Ils sont faciles et compréhensibles par tous les acteurs de l’entreprise impliqués dans cette modélisation, mais souffrent d’un manque de formalisme qui peut produire des incohérences et un dysfonctionnement des processus modélisés, et ne permettent pas d’autre part d’effectuer une analyse et une vérification, pour cela nous proposons une transformation des diagrammes d’activités d’UML vers leurs équivalents dans un modèle formel tel que les réseaux de Pétri, qui représente un outil formel pouvant être utilisé comme une base pour une éventuelle vérification et analyse afin de garantir la cohérence et le bon fonctionnement d’un workflow.