Identifiant pérenne de la notice : 247846422
Notice de type
Notice de regroupement
Note publique d'information : 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 .
Note publique d'information : 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
paprika.idref.fr
data.idref.fr
Documentation
