en fr Alloy4PV : a Framework for Business Process Verification Alloy4PV : un Framework pour la Vérification de Procédés Métiers Reportar como inadecuado




en fr Alloy4PV : a Framework for Business Process Verification Alloy4PV : un Framework pour la Vérification de Procédés Métiers - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LIP6 - Laboratoire d-Informatique de Paris 6

Abstract : 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.

Résumé : 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é.

en fr

Keywords : First-order logic Business

Mots-clés : Procédés Métiers Alloy Logique de premier-Ordre Model-Checking Vérification





Autor: Yoann Laurent -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados