| Titre : | Vérification paramétréee à partir des spécifications formelles des systèemes d’information |
| Auteurs : | Sara Houhou, Auteur ; Souheib Baarir, Directeur de thèse ; Salaun Gwen, Directeur de thèse |
| Type de document : | Thése doctorat |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2022 |
| Format : | 1 vol. (169 p.) / ill., couv. ill. en coul / 30 cm |
| Langues: | Français |
| Mots-clés: | BPM, BPMN, Collaboration, Communication, Temps, Sémantique Formelle, Vérification, Outil, TLA+, Alloy |
| Résumé : |
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. |
| Sommaire : |
Acknowledgement v Abstract vii Résumé viii Contents ix 1 Introduction 1 1.1 Thesis Context . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Motivation and Problem Statement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Research Contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.4 Thesis Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.5 List of Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 I State of the Art 7 2 Background 9 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2 Business Process Management (BPM) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.3 Business Process Modelling Language (BPMN) . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3.1 BPMN Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3.2 Running Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.3.3 BPMN XML Representation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.3.4 BPMN Operational Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.4 First-Order Logic (FOL) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.4.1 Syntax of First-Order Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.4.2 Semantics of First-Order Logic Formulas . . . . . . . . . . . . . . . . . . . . . . . . 25 2.5 Verification Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.5.1 Test . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.5.2 Abstract Interpretation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.5.3 Theorem Proving . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.5.4 Model-Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.6 Verification Languages & Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.6.1 TLA Logic and TLA+ Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2.6.2 Alloy Logic & Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 3 Literature Review 41 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 3.2 Research Method . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.2.1 Objectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.2.2 Survey questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.2.3 Prior Reviews on Business Process Modelling Verification . . . . . . . . . . . . . . 42 3.2.4 Research Strategy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.2.5 Article Selection and Inclusion and Exclusion Criteria . . . . . . . . . . . . . . . . 44 3.3.1 Approaches based on Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 3.3.2 Approaches based on Automata Theory . . . . . . . . . . . . . . . . . . . . . . . . 48 3.3.3 Approaches based on Process Algebras . . . . . . . . . . . . . . . . . . . . . . . . . 50 3.3.4 Approaches based on Logic Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . 51 3.3.5 Approach based on a Programming Language . . . . . . . . . . . . . . . . . . . . . 53 3.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 II BPMN 2.0 Semantics Formalisation 65 4 BPMN and Communication 67 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 4.2 A Typed Graph Representation of BPMN Collaborations Models . . . . . . . . . . . . . . 68 4.2.1 BPMN Elements Type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 4.2.2 Graph Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 4.2.3 Well-formed BPMN graph. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 4.3 A Communication Model Representation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 4.3.1 Communication Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 4.3.2 Communication Channel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 4.3.3 Generic Communication Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 4.4 A FOL Semantics for BPMN Collaborations . . . . . . . . . . . . . . . . . . . . . . . . . . 78 4.5 Verification Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 5 BPMN and Time 99 5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 5.2 A Typed Graph Representation of BPMN Time-Related Constructs . . . . . . . . . . . . 100 5.3 A FOL Semantics for BPMN Time-Related Constructs . . . . . . . . . . . . . . . . . . . . 102 5.3.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 5.3.2 Transition Relation and Executions . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 5.4 BPMN 2.0 and the Time Patterns: Can We Support All of Them? . . . . . . . . . . . . . 114 5.4.1 Time Lags between Activities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 5.4.2 Duration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 5.4.3 Time Lags between Arbitrary Events . . . . . . . . . . . . . . . . . . . . . . . . . . 117 5.4.4 Fixed Date Elements (Deadline) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 5.4.5 Schedule Restricted Element . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 5.4.6 Time Based Restrictions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 5.4.7 Validity Period . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 5.4.8 Time Dependent Variability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 5.4.9 Cycle Element . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122 5.4.10 Periodicity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 III From Formal Semantics to Tool Support 125 6 fbpmn: Formal BPMN Framework 127 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 6.2 fbpmn Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 6.3 Encoding of FOL Semantics in TLA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 6.3.1 Communication as a Parameter. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131 6.3.2 Mechanised Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131 6.4 Encoding of the Semantics in Alloy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 6.4.1 Mechanised verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 6.5 fbpmn Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 6.5.1 Experiments using the TLA+ Encoding/Tooling . . . . . . . . . . . . . . . . . . . 138 6.5.2 Experiments using the Alloy Encoding/Tooling . . . . . . . . . . . . . . . . . . . . 140 6.6 The fbpmn Supporting Tool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142 6.6.1 Architecture and General Principles . . . . . . . . . . . . . . . . . . . . . . . . . . 142 6.6.2 Desktop Modelling and Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . 142 6.6.3 Online Modelling and Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . 144 6.6.4 Extensibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144 IV Conclusion and Future Work 147 7 Conclusion 149 7.1 Objectives Remainder . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 7.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 7.3 Position with Reference to the Litterature . . . . . . . . . . . . . . . . . . . . . . . . . . . 150 7.3.1 Collaboration-Based Approaches . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150 7.3.2 Time-Based Approaches . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150 7.4 Limitations & Perspectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152 Bibliography 155 |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| TINF/194 | Théses de doctorat | bibliothèque sciences exactes | Consultable |
