Supervision : Pascal POIZAT, Laîd KAHLOUL

Co-supervision : BAARIR Souheib

Parameterised Verification from Formal Specifications of Information Systems

Business process models verification is crucial to detect possible errors in design time, rather than at execution on business process engines. BPMN is the primary notation for business process modeling. It is an ISO standard, widely used both in education and in industry. The semantics of BPMN are however defined in a semi-formal way within the standard. This is why many works have tackled the definition of formal semantics for BPMN. In this thesis, we first provided a detailed study of the main works relating to the verification of BPMN models. This allowed us to identify several fragments of the notation which are often put aside in the work of formalization, such as the different models of communication, the temporal management, or the multi-instance character. These aspects are, however, crucial for the extension of the field of application of BPMN to frameworks such as the Internet of Things or the Factory of the Future. We then defined an approach to the verification of business processes collaboration models that supports several of these perspectives, namely the different communication models and time constraints. For this, we have defined formal execution semantics, in terms of first-order logic, to the BPMN fragment taken into account. We then defined implementations of this semantics in the formal languages ??TLA + and Alloy. Finally, this enabled the models to be verified using tools dedicated to these formal languages. Our approach is supported by a tool, fbpmn, allowing the formal transformation of BPMN models to TLA + and Alloy, the verification of models, and the animation of counter-examples when the properties to be verified are not satisfied. This feedback is done directly on the initial BPMN model which makes the approach practicable in the context of use by non-specialists of formal methods. A web application has also been developed to make it even easier to apply our formal approach in an industrial setting. Our tools, our TLA + and Alloy formal semantics implementations, and our library of examples are open sources and available online.

2019-2022 Publications

• 2022
  • S. Houhou, S. Baarir, P. Poizat, Ph. Quéinnec, L. Kahloud : “A First-Order Logic Verification Framework for Communication-Parametric and Time-Aware BPMN Collaborations”, Information Systems, vol. 104, pp. 101765, (Elsevier) (2022)
• 2021
  • S. Houhou : “Parameterised Verification from Formal Specifications of Information Systems”, thesis, phd defence 12/22/2021, supervision Poizat, Pascal Kahloul, Laîd, co-supervision : Baarir, Souheib (2021)
  • R. Saddem‑Yagoubi, P. Poizat, S. Houhou : “Business Processes Meet Spatial Concerns: the sBPMN Verification Framework”, FM 2021 - 24^th International Symposium on Formal Methods, vol. 13047, Lecture Notes in Computer Science, Beijing, China, pp. 218-234 (2021)
  • S. Houhou, S. Baarir, P. Poizat, Ph. Quéinnec : “A Direct Formal Semantics for BPMN Time-Related Constructs”, ENASE 2021 - 16^th International Conference on Evaluation of Novel Approaches to Software Engineering, online, Czechia, pp. 138-149 (2021)
• 2019
  • S. Houhou, S. Baarir, P. Poizat, Ph. Quéinnec : “A First-Order Logic Semantics for Communication-Parametric BPMN Collaborations”, BPM 2019: Business Process Management, vol. 11675, Lecture Notes in Computer Science book series (LNCS), Vienna, Austria, pp. 52-68 (2019)