PhD graduated
Team : MoVe
    Sorbonne Université - LIP6
    Boîte courrier 169
    Couloir 25-26, Étage 2, Bureau 220
    4 place Jussieu
    75252 PARIS CEDEX 05

Tel: +33 1 44 27 31 92, Sara.Houhou (at) nulllip6.fr

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.

Defence : 12/22/2021 - 14h - Campus Pierre et Marie Curie - 25-26/105 ou zoom https://umontpellier-fr.zoom.us/j/9902563240

Jury members :

RE Barbara (Maître de conférence à Camerino Université, HDR, PROS) [Rapporteur]
SALAÜN Gwen (Professeur à Grenoble Alpes Université, LIG, CNRS) [Rapporteur]
BÉRARD Béatrice (Professeur à Sorbonne Université, LIP6, CNRS)
HAMZA Lamia (Maître de conférence à Bejaia Université, HDR, LIMED)
OKBA Tibermacine (Maître de conférence à Biskra Université, HDR,LESIA)
BAARIR Souheib (Maître de conférence à Paris Nanterre Université, HDR, LIP6, CNRS)
KAHLOUL Laîd (Professeur à Biskra Université, LINFI)
POIZAT Pascal (Professeur à Paris Nanterre Université, LIP6, CNRS)

2019-2021 Publications