Description
Date depot: 11 avril 2023
Titre: Formal Verification of Business Process Models and Notations.
Directeur de thèse:
Souheib BAARIR (LRE)
Encadrant :
Quentin PEYRAS (LRE)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Modèles de calcul, preuve, vérification
Resumé: Business process modeling is a valuable framework that allows companies and organizations to exert greater control over their processes. In the field of process notation, Business Process Model and Notation (BPMN) is among the most popular. Various initiatives have proposed formal semantics for BPMN, including a recent first-order logic formalization. Using this formalization, it is possible to translate the semantics into a specification language for verification purposes. Verification is important as it enables formal checking of critical properties of BPMN, such as dead transitions (transitions that are never taken), deadlocks (the process is blocked and cannot perform a transition), and livelocks (the process is stuck in a loop preventing it from completing its task). Moreover, time constraints are of utmost importance in BPMN, and thus, must be taken into account for verification purposes. Therefore, the formalization must include the semantics of time-related constructs, allowing for quantitative verification in addition to qualitative verification. Some recent works encode the resulting semantics in TLA+, a well-known specification language, and use the TLA+ model-checker, TLC, to verify properties related to BPMN. While this formalization shows promise, it does not cover all aspects of BPMN semantics, such as unbound data, multi-instance constructs or variable duration for tasks, leaving room for future research.