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

Business Process Management

Il a été largement reconnu que l’utilisation de procédés métiers au sein d’une entreprise permet de fournir des produits et des services de manière plus ecace [277]. En capturant l’ordonnancement des activités, le flux d’informations des données requises et produites, les modèles de procédé décrivent de manière détaillée les interactions entre les diérents participants du procédé [265, 277]. La gestion de procédés métiers (BPM, pour Business Process Management) a été définie par Van der Aalst comme une façon de “… supporter les procédés métiers en utilisant des méthodes, techniques, et logiciels pour modéliser, exécuter, contrôler, et analyser les procédés opérationnels impliquant des humains, organisations, applications, documents ou toute autre source d’informations” [260]. Les modèles de procédés représentent donc une part essentielle du patrimoine des entreprises et constituent leur plus grand facteur de réussite. Les systèmes BPM (BPMSs) sont des outils logiciels destinés à automatiser la mise en application de ces procédés. Lorsque l’un de ces systèmes est déployé au sein d’une entreprise, cela a un impact significatif sur la productivité de l’entreprise. La figure 1.1 montre le cycle de vie classique de la gestion des procédés métiers. Ce cycle commence par la modélisation du procédé, où celui-ci est identifié, examiné, validé, et finalement représenté sous forme de modèle  de procédé [277]. Généralement, les modèles de procédés sont développés en utilisant un langage de modélisation (PML, pour Process Modeling Language), p. ex., Business Process Modeling Notation (BPMN) [192], Business Process Execution Language (BPEL) [133], Unified Modeling Language (UML) [190], Software Process Engineering Metamodel (SPEM) [188], etc. Ensuite, le modèle de procédé est utilisé pour configurer les informations au sein du système, ex., assigner les activités aux employés. Dans la phase d’exécution, le procédé doit être exécuté au sein de l’organisation en suivant la voie prescrite par la modélisation du procédé. La dernière phase de diagnostic utilise les informations résultant de l’exécution afin de l’évaluer. Ce résultat est utilisé pour fermer le cycle BPM dans le but de continuellement améliorer le procédé [36], selon le diagnostic, certaines parties du procédé peuvent être remodélisées. L’objectif principal des BPMSs est donc de supporter complètement ce cycle de vie.

Complexité et contraintes de modélisation

L’adoption croissante des BPMSs dans les entreprises encourage une automatisation toujours plus poussée des procédés métiers. Certains modèles de procédés peuvent atteindre plus de 250 activités [34] contenant un flux de contrôle complexe impliquant boucles, synchronisation et dépendances entre les données et ressources [103]. En eet, la figure 1.2 montre que les modèles de procédés sont régis principalement par 3 perspectives : le flux de contrôle, les ressources et les données. Sur cette figure, le modèle est un exemple simple contenant 3 activités pour enregistrer un album dans la base de données. La perspective de flux de contrôle définit l’ordre d’exécution des activités [268, 218]. La perspective des ressources détermine quelles ressources (humaines ou non) sont autorisées à exécuter chacune des activités ainsi que leurs allocations par rapport à celles-ci [268, 84, 219, 217]. La perspective des données définit quelles données sont disponibles dans le procédé et comment les utilisateurs peuvent y accéder lors de l’exécution [268, 216]. De plus, les modèles de procédés possèdent souvent une liste de contraintes spécifiques au projet ou à l’entreprise. Par exemple, certains modèles contiennent des informations concernant le temps aecté à chacune des activités ainsi que la disponibilité des ressources [69, 149]. Pour toutes ces raisons, la modélisation de procédé est une tâche complexe et est facilement sujette aux erreurs, même pour un expert dans le domaine [268]. D’autre part, le cycle de vie des modèles de procédés est loin d’être trivial. Après avoir été modélisés dans la phase de modélisation, ces modèles peuvent être modifiés à la volée pendant la phase d’exécution [208, 199, 50] afin de prévenir le besoin de futures déviations du modèle [46, 135, 49]. En eet, dans certains domaines de procédés métiers, il n’est pas toujours possible de modéliser un modèle de procédé anticipant toutes les situations possibles qui pourraient arriver pendant l’execution. Par exemple, dans le cas d’utilisation de procédé de développement logiciel, Lanubile et Vissagio ont montrés que 98% des agents dévient, peu importe le procédé utilisé (ex. scum, rup …) [148]. De plus, ces modèles sont une nouvelle fois sujets à des ranements dans la phase de diagnostic par souci d’amélioration et de correction du modèle pour la prochaine exécution [231, 52, 36]. Il est de notoriété publique qu’il est préférable de détecter les problèmes logiciels le plus tôt possible, de préférence avant leurs mises en production [182]. Dans le cas des procédés métiers, ceci est particulièrement important du fait qu’ils impactent directement le cœur du fonctionnement de l’entreprise. Du fait que tout le cycle de vie BPM est dirigé par ces modèles de procédés, leur exactitude est cruciale. “Le procédé est-il correct ?”. Comme toute autre activité intellectuelle impliquant l’homme, un modélisateur peut introduire certaines erreurs ou incohérences lors de la modélisation. Une erreur de modélisation peut, en plus d’entraîner une perte de temps et d’argent, entraver le bon fonctionnement de l’entreprise et mener à un déclin dans la qualité des produits et services délivrés. De toute évidence, plus une erreur est détectée tard, plus une partie du travail à refaire sera importante.

Modèles erronées

Comme indiqué dans de nombreuses études, les modélisateurs de procédés tendent à faire beaucoup d’erreurs. Par exemple, l’étude [173] montre que sur plus de 2000 modèles de procédés, 10% des modèles sont imparfaits et comportent des erreurs comportementales. Les modèles SAP, un ensemble public de modèles contenant plus de 600 procédés non triviaux exprimés en terme d’EPC (Event-Driven Process Chains), a montré un taux d’erreurs de plus de 20% [172, 171]. Gruhn et al. [104] ont collecté 285 EPCs à partir de diérentes sources (thèses, master, papiers scientifiques, thèses de doctorat…) et sont arrivés à la conclusion que plus de 38% des procédés contenaient des erreurs comportementales. Vanhatalo et al. [269] ont analysé le flux de contrôle de plus de 340 procédés métiers modélisés avec IBM WebSphere Business Modeler [121] pour découvrir que plus de la moitié d’entre eux n’étaient pas sûrs. Des erreurs classiques peuvent consister en des inters-blocages, des activités jamais exécutées, une donnée ou une ressource non disponible au démarrage d’une activité, un manque de temps pour eectuer les activités, etc. Bien que les procédés métiers soient utilisés depuis plus d’une vingtaine d’années [145], force est de constater que ces récentes études soulignent l’incapacité des outils de modélisation à capturer certaines de ces erreurs.

Besoin de vérification

Idéalement, après chacune des modifications apportées aux modèles, le procédé est analysé et vérifié afin de garantir son exactitude [270, 261]. Cette vérification doit être non seulement capable de relever les erreurs classiques communes à tous les procédés tels que les inter-blocages, mais aussi de s’assurer que les contraintes relatives à l’entreprise, au projet et au domaine (p. ex. médical, militaire, entreprise, développement logiciel) [19] soient respectées et préservées pendant tout le cycle de vie du procédé. Des modèles de procédés ecaces et fiables font partie des points clés pour le succès des entreprises modernes. Cependant, sans outils proposant une vérification automatique et exhaustive du procédé, il est impossible pour un expert du domaine de se faire une représentation mentale de tous les chemins possibles d’exécutions et de garantir que certaines propriétés essentielles sont respectées par le modèle. Une façon d’eectuer cette analyse consiste à recourir à des techniques de vérification formelle, telles que le model-checking : une technique pour la vérification automatique de systèmes réactifs introduite par Clarke et al. [40, 42]. L’approche consiste à définir formellement le modèle de procédé et sa sémantique, ainsi que la propriété à vérifier. Ensuite, ces deux entités sont envoyées à ce que l’on appelle un model-checker, qui va répondre à la question de satisfiabilité de la propriété par le modèle en explorant exhaustivement l’espace d’état. Dans le cas où la propriété n’est pas vérifiée, un contre-exemple est généré par le model checker. Bien que de nombreuses approches aient été proposées pour vérifier des procédés, aucune technique de vérification n’a réussi à s’imposer et à détrôner les autres [179]. Leurs complexités [103], l’utilisation de formalisme mathématique et l’impossibilité pour un simple modélisateur de procédés d’utiliser et de comprendre ces outils ont été parmi les obstacles majeurs à leurs adoptions [171]. Afin de définir plus précisemment les principaux problèmes que nous avons identifiés, prenons comme exemple un procédé de la spécification UML. La figure 1.3 montre ce procédé modélisé en utilisant les diagrammes d’activités UML. Le but de ce procédé est de gérer la réception d’une commande au sein d’une entreprise. Ce procédé comporte 7 actions (ReceiveOrder, FillOrder…) reliées par diérents noeuds de contrôle (DecisionNode, ForkNode …) pour représenter la perspective du flux de controle. Les données sont représentées à l’aide d’épingles (pins) attachés aux actions (InputPin/OutputPin). Certaines informations organisationnelles sont attachées aux actions telles que les resources utilisées par les actions (ex. BankConnector), ainsi que le temps nécessaire pour les eectuer. Dans la suite, nous catégorisons en deux sous-ensembles les types de problèmes liés aux approaches de la littératures : (a) la formalisation utilisée et (b) leurs mises en application.

Table des matières

1 Introduction
1.1 Business Process Management
1.2 Objectifs de la thèse
1.3 Structure du document
1.4 Publications
2 Contexte et État de l’art
2.1 Concepts et définitions
2.2 Propriétés à vérifier pour garantir la conformité d’un procédé
2.3 Comparaison des approches de vérification
2.4 Expression de propriétés métiers sur un modèle de procédé
2.5 Conclusion et synthèse générale
3 Formalisation de UML AD et fUML
3.1 Foundational UML (fUML)
3.2 Formalisation de UML AD et fUML
3.3 Formalisation des propriétés pour la vérification d’un procédé
3.4 Conclusion
4 Alloy4PV : Un framework basé sur Alloy
4.1 Alloy : un langage et un outil
4.2 Alloy4PV : Un framework pour la vérification de procédés
4.3 Outil graphique associé à Alloy4PV
4.4 Conclusion
5 Generation de procédés
5.1 Motivations
5.2 Idées pour représenter et générer un procédé
5.3 Genetic Algorithm
5.4 Utilisation d’un algorithme genetique pour la génération de procédés
5.5 Validité des procédés générés
5.6 Prototype
5.7 Évaluation
5.8 Travaux connexes
5.9 Conclusion
6 Evaluation
6.1 Accomplissement des objectifs
6.2 Performance
6.3 Conclusion
7 Conclusion

Télécharger le rapport complet