Inria center of University Grenoble Alpes and LIG (FRANCE)
Quantitative analysis of business processes.
CADP (Construction and Analysis of Distributed Processes)
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.
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.
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
Inria center of University Grenoble Alpes / CONVECS team
655, avenue de l'Europe
F-30330 Montbonnot Saint Martin
|This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software