Vérification de spécifications modales de réseaux worklows à l'aide de solveurs de contraintes et de methodes de résolution

Nowadays workflows are extensively used by companies and organisations in order to improve organizationaleffciency, responsiveness and profitability by managing the tasks and steps of business processes. Theverification of specifications has become mandatory to ensure that such processes are properly designedand reach the expected level of trust and quality. In this context, this thesis addresses the verification ofmodal specifications – necessary or admissible behaviour involving several activities and their causalities –of workflow nets – a Petri nets class suited for the description of workflows.In particular, it defines an innovative constraint system based framework to model executions of ordinary as wellas coloured workflow nets, and verify modal specifications. Further, it presents powerful reduction methodspreserving properties of interest such as generalised soundness and correctness of a given modal specification.Such reduction methods are then portrayed as pre-processing steps reducing workflow nets size, so that theverification of preserved properties can be carried out on smaller instances.Finally, as a practical contribution, this thesis introduces the tools that have been implemented as well asexperimentations that have been carried out over industrial workflow nets in order to validate the approachesproposed in this thesis. The convincing experimental results highlight the effectiveness, effciency andscalability of the modal specification verification method and reduction methods introduced in this thesis.De nos jours, les workflows sont largement utilisés par les entreprises et les organisations en vue d’améliorer l’efficacité organisationnelle, la réactivité et la rentabilité en gérant les tâches et les étapes de processus opérationnels. La vérification des spécifications est devenue obligatoire afin d’assurer que ces processus sont correctement conçus et atteignent le niveau de confiance et de qualité attendu.Dans ce contexte, cette thèse porte sur la vérification de spécifications modales – comportements nécessaires ou recevables impliquant plusieurs activités et leurs causalités – de workflows nets – une classe de réseaux de Petri adaptés à la description de workflows. En particulier, cette thèse définit un cadre novateur permettant de modéliser les exécutions de workflow nets,avec ou sans données, et de vérifier des spécifications modales à l’aide de systèmes de contraintes. Elle présente également deux méthodes de réduction préservant la "generalised soundness" et la validité d’une spécification modale donnée. Ces méthodes de réduction sont ensuite présentées comme des étapes de prétraitement réduisant la taille des workflow nets, de sorte que la vérification des propriétés conservées puisse être effectuée sur de plus petites instances. Enfin, cette thèse présente les outils qui ont été mis en oeuvre ainsi que des expérimentations qui ont été menées sur un grand nombre de workflows industriels afin de valider les approches proposées dans cette thèse. Ces résultats expérimentaux convaincants mettent en évidence l’efficacité, l’efficience et le passage à l’échelle de la méthode vérification de spécification modales ainsi que des méthodes de réduction introduites dans cette thèse