Alloy4PV : un Framework pour la Vérification de Procédés Métiers

In this thesis, we realized a study of the start-of-the-art on different process domains (business, software, military, medical, etc.). The aim was to identify and categorize critical properties that can be verified on any process model. This study resulted in a library of generic and configurable properties. As a second step, we have defined a framework for process verification called Alloy4PV. This framework uses a subset of UML 2 Activity Diagram as a process modeling language. For process verification, (1) we defined a formal model of UML 2 Activity Diagram based on the fUML semantics, the OMG standard that gives a semantic to a subset of UML 2. This was achieved using first-order logic, (2) we implemented this formalization using the Alloy language in order to perform bounded model-checking, and (3) we automatized in a graphical tool integrated to Eclipse, the possibility to express and verify properties on all the perspectives of a process model. This contribution resulted in a tool which is under evaluation by our MerGE project’s partners and to five publications in conferences proceedings.Dans cette thèse, nous avons tout d'abord fait une étude de l'état de l'art dans les différents domaines des procédés (métier, logiciel, militaire, médical, etc) afin d'identifier et de catégoriser les principales propriétés à garantir. À partir de cette étude, nous avons défini une bibliothèque de propriétés générique et paramétrable pour tout modèle de procédé. Ensuite, nous avons défini un framework pour la vérification de procédés appelé Alloy4PV. Il utilise un sous-ensemble des diagrammes d'activités UML 2 comme langage de modélisation. Afin d'effectuer la vérification de procédés, nous avons (1) défini un modèle formel des diagrammes d'activités basé sur la sémantique fUML (le standard de l'OMG donnant une sémantique à un sous-ensemble de UML) en utilisant la logique de premier ordre, (2) implémenté cette formalisation en utilisant le langage Alloy afin d'effectuer du model-checking borné, et (3) automatisé, dans un outil graphique intégré à Eclipse, la possibilité d'exprimer et de vérifier des propriétés sur toutes les perspectives du procédé