Skip to main content

Ahang Zuo

Thursday, April 11th ,2024

Modelling, Runtime Analysis and Quantitative Verification of Business Processe

Abstract:

Business processes are structured tasks that model a specific service or product. The optimisation of these processes is a strategic activity in organisations because of its potential to increase profit margins and reduce operating costs. Business Process Model and Notation (BPMN) is the de facto standard modelling language for developing business processes, which defines the set of tasks involved in a process and the order in which they should be executed. The main contributions of this thesis are: (i) Building an optimised process with BPMN language is not easy for non-expert users due to the lack of support at design time. The first contribution presents an approach to support such users in building optimised processes. An abstract graph, which describes an abstract version of a process, is first generated by defining the set of tasks and a partial order between some of them. The user can then successively refine this abstract graph. Refinement is guided by the minimum and maximum execution times needed for executing the whole process. Once the user is satisfied, the last step transforms this graph into a BPMN process. (ii) Resources are necessary for executing some specific tasks of a running process, knowing the probabilities associated with specific tasks is essential for adjusting resources and thus optimising costs. In addition, it is particularly difficult to ensure correctness and efficiency of the multiple executions of a process. The second contribution proposes to rely on Probabilistic Model Checking (PMC) to automatically verify that multiple executions of a process respect some specific probabilistic property. This approach applies at runtime, thus the evaluation of the property is periodically verified and the corresponding results updated. Furthermore, we propose a probabilistic runtime enforcement mechanism to keep executing the process while avoiding the violation of the property. (iii) A well-defined resource allocation strategy is essential for optimising waiting times and costs by mitigating delays and enhancing resource utilisation. The third contribution presents a generic approach to dynamically adjust resource allocation during the execution of BPMN processes. In addition, we introduce a strategy relying on a predictive model for computing metrics of interest, including resource usage and average execution time, which allows us to anticipate the change in resources and thus improve by reducing process execution time, costs associated with resources and have a more balanced usage of resources.

Date et lieu

Thursday, April,11t, 2024 at 14h
Grand Amphi of Inria Grenoble
and Zoom

 

 

Jury members

Pascal POIZAT
Université Paris Nanterre Rapporteur Reviewer

Pascale LE GALL
Université Paris Saclay Reviewer

Olga KOUCHNARENKO
Université de Franche-Comté Examiner

Yves LEDRU
Université Grenoble Alpes Examiner

Gwen SALAÜN
Université Grenoble Alpes Supervisor

Yliès FALCONE
Université Grenoble Alpes Co-Supervisor - invited

Submitted on April 9, 2024

Updated on April 9, 2024