Vérification paramétréee à partir des spécifications formelles des systèemes d’information

Sara, Houhou (2021) Vérification paramétréee à partir des spécifications formelles des systèemes d’information. Doctoral thesis, Université Mohamed Khider (Biskra - Algérie).

Text these_archivage_N°3779961.pdf Download (10MB)

Abstract

Les modéles de processus sont des outils essentiels pour l’apprentissage, l’analyse, l’amélioration et la communication autour d’un processus métier. BPMN est la norme standard pour la modélisation de processus métiers. Il fournit une notation compréhensible par les utilisateurs métier, allant des analystes métier qui désignent les ébauches initiales des processus aux développeurs techniques chargés de les mettre en oeuvre, et enfin au personnel qui déploie et surveille ces processus. BPMN supporte la modélisation à l’aide de différents types de diagrammes, parmi lesquels le diagramme de collaboration. Ce dernier fournit un moyen efficace de décrire comment plusieurs entités, chacune avec son propre processus interne, peuvent collaborer et interagir les unes avec les autres pour ôatteindre des objectifs. Même s’il s’agit d’une notation largement admise, la sémantique d’exécution de BPMN est définit en langage naturel. Cela laisse place à l’interprétation et limite l’analyse formelle possible des modèles. Un gros effort a été consacré à proposer une sémantique formelle pour BPMN et, dans une moindre mesure, à fournir des outils de vérification dédiés. Cependant, certaines fonctionnalités avancées de BPMN, à savoir les sous-processus, la communication ou les constructions liées au temps, sont souvent laissées de côté. Cela constitue un problème car BPMN a suscité l’intérêt en dehors de son champ d’application-initial, par exemple pour l’Internet des objets (IoT) où la communication et le temps jouent un rôle important. La modélisation d’un diagramme BPMN, ainsi que la garantie complète de son comportement, peuvents’avérer très difficiles à assurer en présence de tels concepts. Pour cela, il est nécessaire de fournir une sémantique formelle prenant en compte non seulement les constructions de processus habituelles, mais également celles liées aux sous-processus, à la communication inter-processus et au temps. D’autre part, la complexité des outils associés, leur absence de prise en charge entièrement automatique de l’ensemble de la chaîne de vérification, le fait qu’ils ne soient pas intégrés dans un environnement de processus et l’impossibilité pour le modélisateur moyen de processus d’exprimer des propriétés métier empêchent leur adoption. Dans cette thèse, nous proposons des solutions à ces problèmes en fournissant une sémantique formelle en logique de premier ordre pour les diagrammes de collaboration de BPMN qui prend en charge les constructions liées aux sous-processus, à la communication et au temps. Cette sémantique est paramétrique par rapport sept modéles de communication point à point qui existent lorsque l’on considère l’ordre local et global des messages. Nous avons implémenté cette sémantique dans une suite d’outils appelée fbpmn. Elle permet d’effectuer la vérification automatique des propriétés de correction pour les modèles de collaboration BPMN et d’animer les modèles des contre exemples lorsque les propriétés ne sont pas satisfaites. Notre cadre logiciel est basé sur deux languages de spécification formelle différents. Une première implémentation de la sémantique utilise le langage TLA+. Il est accompagné de plusieurs outils, dont le model checker TLC qui prend en charge la vérification de modèle explicite. L’expressivité de TLA+ vient du fait qu’il est basé sur ZF (théorie des ensembles), la logique du premier ordre et des modules paramétrables. La deuxième implémentation de la sémantique est basées sur le langage Alloy. Il est accompagné d’ Alloy Analyser qui prend en charge la vérification de modèle bornée. L’expressivité d’Alloy vient du fait qu’il est basé sur une logique relationnelle, une logique de premier ordre renforcée par l’opération de fermeture transitive, ce qui rend la définition des propriétés structurelles extrêmement simple. Tous ces outils, l’outil fbpmn, l’outil TLC et Alloy Analyser peuvent être utilisés pour effectuer la vérification des propriétés spécifiques aux workflows de modéles BPMN. La suite d’outils fbpmn est open source et disponible gratuitement en ligne.

Actions (login required)

View Item