Modélisation et analyse des processus Workflows reconfigurables et distribués par les ECATNets récursifs
Institution:
Paris, CNAMDisciplines:
Directors:
Abstract EN:
In this thesis, we propose a new model for the modeling and the analysis of distributed and reconfigurable worklow processes, namely Recursive ECATNets (RECATNets). RECATNets are sound combination of the ordinary ECATNets (Extended Concurrent Algebraic Terms Nets) and the recursive Petri nets. The interest of RECATNets which we precise their syntax and semantics, is to offer a reursive mechanism appropiate for the modeling of the dynamic creation and suppression of processes. We show also, via this model, the verification of the correction criteria of workflow processes (soundness and compatibility). The semantic of RECATNets is described in terms of rewriting logic allows the rapid prototyping and the formal verification of these properties using the Maude system. We propose also a temporal extension of the RECATNets model for the explicit representation of time constraints of reconfigurable workflows. For a complete verification, we also develop a method for the construction of the state class graph of the T-RECATNets and implement it in the framework of the rewriting logic
Abstract FR:
Dans cette thèse, nous proposons un nouveau modèle pour la modélisation et l'analyse des processus workflows reconfigurables et distribués, appelé ECATNet récursif (RECATNet). Les RECATNets sont une combinaison saine des ECATnets ordinaires (Extended Concurrent Algebraic Terms Nets) et des réseaux de Petri récursifs. L'intérêt majeur des RECATNets, dont nous précisons la syntaxe et la sémantique, est d'offrir un mécanisme récursif approprié à la modélisation de la création et de la suppression dynamique de processus. Nous montrons aussi à travers ce modèle la vérification des critères de correction des processus workflows (la cohérence et la compatibilité). La sémantique des RECATNets traduite en termes de lal ogique de réécriture nous permet le prototypage rapide et la vérification formelle de ces prpriétés à l'aide de l'outil de réccriture Maude. Nous proposons aussi une expension temporelle du modèle des RECATNets pour la repréensation explicite des contraintes de temps liées aux workflows reconfigurables. Pour une analyse complète, nous avons développé une méthode de construction du graphe des classes d'états spécifique aux T-RECATNets que nous avons implémenté dans le cadre de la logique de réécriture.