Probabilistic Model Checking of BPMN Processes at Runtime

Organisation:	Inria center of University Grenoble Alpes and LIG (FRANCE)
Functionality:	Quantitative analysis of business processes.
Tools used:	VBPMN CADP (Construction and Analysis of Distributed Processes)
Period:	2022
Description:	BPMN (Business Process Model and Notation), proposed by OMG, is the de facto standard for developing business processes. BPMN relies on a graphical workflow-based notation that describes the structured tasks in a business process and the relationships between these tasks. The execution of one task or another is influenced by the use of different kinds of gateways (e.g., exclusive) in the BPMN process. The probabilities of executing certain tasks (or combinations thereof) when running the process are difficult to determine, especially when multiple instances of the process are executed at the same time. In that case, since resources are necessary for executing some specific tasks, knowing these probabilities is of prime importance for better adjusting the corresponding resources and thus converging to an optimal allocation of resources. This work proposed an approach to perform probabilistic model checking of BPMN processes at runtime. A business process (described using an executable version of BPMN) can be executed multiple times. Different executions (instances) may perform different tasks in the process. The approach first monitors these executions to extract from the corresponding logs the probability of executing each individual task. These probabilities are used to build a semantic model of the BPMN process where these probabilities appear explicitly. This PTS (Probabilistic Transition System) model is obtained by translating the BPMN process to LNT using the VPBMN framework, generating the LTS (Labeled Transition System) of the LNT description using the CADP compilers, and decorating the transitions of this LTS with the probabilities computed by monitoring. This PTS model can be exploited to verify probabilistic properties (e.g., the probability of executing a certain task) using the EVALUATOR 5.0 model checker of CADP. Since more instances of the process can keep executing including variations in terms of frequency of the executed tasks, the probabilities of LTS transitions evolve over time. The approach is therefore applied periodically, producing a dynamic curve that indicates the evolution of the probabilistic properties verdicts over time. The approach is illustrated on a BPMN process describing the shipment process of a hardware retailer.
Conclusions:	The proposed approach allows BPMN analysts to automatically carry out probabilistic model checking of BPMN processes at runtime. This is useful for effectively adjusting resource allocation depending on the runtime analysis results.
Publications:	[Falcone-Salaun-Zuo-22] Yliès Falcone, Gwen Salaün, and Ahang Zuo. "Probabilistic Model Checking of BPMN Processes at Runtime". Proc. of the 17th International Conference on Integrated Formal Methods (iFM'2022), Lugano, Switzerland, Lecture Notes in Computer Science vol. 13274, pp. 191-208. Springer Verlag, 2022. Available on-line at: https://inria.hal.science/hal-03665305/en or from the CADP Web site in PDF or PostScript
Contact:	Gwen Salaün Inria center of University Grenoble Alpes / CONVECS team 655, avenue de l'Europe F-30330 Montbonnot Saint Martin FRANCE Email: gwen.salaun@inria.fr
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page