Séminaire CONVECS 2025
Autrans (Isère)

Lundi 24 novembre 2025

10h00 – 10h30

Café d’accueil

10h30 – 11h30

Quentin Nivon

Analysis, Optimisation and Debugging of BPMN Processes

Modelling and designing business processes have become crucial activities for companies in the last decades. Consequently, multiple workflow modelling notations emerged. Among them, the Business Process Modelling Notation (BPMN) is now considered as the de facto standard for process modelling. The BPMN notation requires a certain level of expertise to allow one to write correct and well-structured processes compliant with some expected requirements. The BPMN modelling phase can thus become tedious, and even error-prone if carried out by non-experts. The first part of this thesis consists in providing a solution to help users modelling BPMN processes. To achieve this goal, the proposed approach takes as input the requirements of the user in a textual format, in which the tasks and their ordering constraints are informally described. It then makes use of Large Language Models (LLMs) to translate these constraints into a machine-readable format. From this internal format, the approach generates and returns a BPMN process satisfying these constraints. As a side contribution, this thesis also presents techniques to verify that a process does not deviate from its expected behaviour. Such verifications are usually performed using classical model checking techniques. However, we thought that a user not familiar with the BPMN notation would struggle using such techniques, and more precisely, writing the expected behaviour of the process in the form of temporal logic properties. Thus, the core of this side contribution consists in facilitating the writing of such properties by allowing the user to generate them directly from their textual description.

Recent studies suggested that, once built, business processes are subject to changes throughout their lifetime. In companies, such changes may often lead to non-optimal processes, responsible of issues such that the increase of the execution time or the costs related to them. To be able to optimise processes, there is a need to have at hand an explicit model of their behavior and quantitative features. Thus, beside the processes themselves, usually modelled using workflow-based notations, one must provide, among others, an explicit description of the durations and the resources required by the tasks composing these processes. The second part of this thesis consists in providing a solution based on refactoring techniques, whose goal is to change the structure of the process in order to optimise one or several criteria of interest, such as process execution time, resource usage, or total costs. To do so, the proposed approaches consist of various ingredients. For instance, we propose refactoring patterns, useful for moving the tasks of the process from one place to another while preserving some of its semantics. We also make use of simulation techniques to compute metrics of interest from the execution of (one or several instances of) the process. Similarly, we utilise several exploration algorithms in order to navigate through the space of solutions. In the end, the multiple presented approaches all return an optimised version of the original process given as input.

11h30 – 12h15

Ouadie Khebbeb (joint work with Gwen Salaün)

Dependency-Aware Reconfigurations of Kubernetes Deployments

Deployments in Kubernetes can rely on services of other deployments, forming implicit dependencies, but Kubernetes lacks the concept of dependencies between deployments. Consequently, performing reconfigurations on deployments (e.g., replacing a deployment with another one) without a proper coordination with their dependents often leads to failures. Whilst Kubernetes features a self-healing mechanism, it is not designed for dependency-aware reconfigurations, and can thus result in either inefficient or even unstable recoveries at scale. To address this, we propose an approach that allows to model Kubernetes deployments and their dependencies in the form of a dependency graph, and enables the expression of reconfiguration intents through a high-level, declarative language. This approach then allows to generate a plan of low-level operations that apply the desired reconfiguration, coordinated with respect to the dependencies.

12h15 – 14h00

Déjeuner et quartier libre

14h00 – 14h45

Radu Mateescu

Expressing Branching-Time and Linear-Time Temporal Properties in MCL

We make a brief account of two temporal logics representative for the branching-time setting (CTL - Computation Tree Logic) and linear-time setting (LTL - Linear Temporal Logic). We illustrate how the properties expressed in these logics can be specified in MCL (Model Checking Language), one of the property languages provided by the CADP toolbox.

14h45 – 15h30

Zachary Assoumani (joint work with Wendelin Serwe)

Connecting Hardware Description Languages and Formal Languages

The growing complexity in critical hardware systems have made the verification requirements even more tight and faultless. In a preliminary study to include formal verification languages in the hardware design flow, we look into the syntactic similarities between LNT and the hardware description language SystemVerilog. Our case study pictures a simple LNT module progressively refined until its syntax is close to SystemVerilog, while preserving the same behavior along the transformations. We finally consider a possible translation between the two languages, to provide a verified rapid prototyping for hardware.

15h30 – 16h00

Pause café

16h00 – 16h20

Wei Chen

Collaborative Modeling with AI: Pedestrian Behaviour in Shared Spaces

This study explores the formal modelling of pedestrian behaviour in shared environments. Through an interactive collaboration with an AI assistant, the research formalises perception, personal space, and social interaction forces in LNT, a formal language for discrete systems. The AI-assisted workflow accelerated model design and implementation while maintaining theoretical consistency with the source literature.

16h20 – 16h40

Aline Uwimbabazi (joint work with Pierre-Yves Lajoie, Lina Marsso, Radu Mateescu, and Wendelin Serwe)

Modeling the Behaviour of Mobile Robots (work in progress)

As research progresses, systems increasingly interact with humans in various domains (e.g., transport, environment, health, and social care). In this research project, we plan to develop a novel framework for safe and efficient robot navigation in highly dynamic indoor environments like hospitals, warehouses, and airports. Indoor environments are dynamic: people move, floor might be wet, robot might have replanned, etc. The robots should react to environmental changes in real-time, ensure both safety and execution of tasks in efficiency way.

We will leverage formal methods, specifically model checking, to systematically generate an exhaustive dataset of provably safe and optimal navigation plans. We will also create probabilistic spatial representations which will encode the movement of objects and the presence of mobile agents, in addition to time-dependent safety constraints. Our research work is still in progress. We present a formal model for assistive-care robotics that helps the human in the daily activities, such as food preparation or calling for help in an emergency situation.

16h40 – 19h00

Quartier libre

19h00

Dîner

Mardi 25 novembre 2025

09h00 – 10h00

Frédéric Lang

Compositional Verification using Sharp Bisimulation

We consider the verification of temporal logic properties on the formal model of a system described as a parallel composition of processes. The well-known state explosion problem may be palliated by compositional verification, a divide-and-conquer approach that consists in generating, reducing with respect to some equivalence relation, and composing the state spaces of individual processes in an incremental way. The choice of the equivalence relation is crucial in that it must compress the state space sufficiently while still preserving the truth value of the property of interest. As such, sharp bisimulation may be tailored in function of the property under verification, so as to get the best compromise between compression and property preservation. Yet, this is in general not easy. I will give hints how to tailor the bisimulation and present a few open problems.

10h00 – 10h30

Pause café

10h30 – 11h30

Hubert Garavel

Variations on a Formal Model of Algorand

Algorand is a promising blockchain technology targeting at decentralization, scalability, security, and energy savings. At the heart of Algorand is a BBA* (generalized Binary Byzantine Agreement) protocol, a formal model of which was developed in LNT by Marco Bernardo and Andrea Esposito (University of Urbino, Italy). Starting from this formal model, we explore many variants of the protocol, by applying both Algorand-specific transformations and LNT-specific transformations, in order to obtain a model as concise as possible. We then verify this model using a combination of techniques supported by CADP, namely visual checking, equivalence checking, and model checking.

11h30 – 12h00

Wendelin Serwe (joint work with Lina Marsso and Radu Mateescu)

Conformance Testing Tools for CADP

In this talk, we present the basic ideas of conformance testing underlying the related tools connected to CADP. We also compare three different implementations.

12h00 – 14h00

Déjeuner et quartier libre

14h00 – 14h30

Gregor Goessler

Causal Explanations for Safety Violations

Causal reasoning aims at establishing causal relationships between events, deemed to be causes, and other events, considered to be effects. Reasoning about causality is often seen as the construction of explanation models for real life phenomena or situations. In this talk, we present the basic definitions of counterfactual causality, the dominant notion in causal reasoning in engineering science, and illustrate their usage for explaining safety violations in concurrent systems.

14h30 – 15h30

Gwen Salaün (joint work with Francisco Durán)

Semantic Comparison of Business Process Models Assisted by Syntactic Matching

A business process describes a set of structured tasks that follow a specific order and results in a product or service. Comparing two different versions of a same process is crucial for tackling several problems such as process analysis, evolution or refactoring. We present new techniques for automatically comparing two BPMN processes from a semantic point of view in an efficient way in terms of computational complexity. To compute this comparison efficiently, our approach detects the syntactic differences between the two processes, and then compares the semantic models of both processes only for these differences. This procedure thus avoids the comparison of the entire semantic models, which may be very costly. The notion of comparison used in this work relies on the congruence of the operators underlying the syntactic matching w.r.t. behavioural equivalences and bisimulations. Our approach is fully automated using a tool chain that we implemented. Experimental results show that the comparison computation is much faster with our approach and tool chain than with other alternative techniques.

15h30 – 16h00

Pause café et fin du séminaire