|
Resource Allocation Analysis of BPMN Processes |
A business process consists of a set of structured activities
that provide a certain service or product. The Business Process
Model and Notation (BPMN) was
published as an ISO
standard in 2013 and has become the de facto
language for developing business processes. Several BPMN
industrial platforms are currently available, but most of them
only support the modeling and simulation of
processes.
Our main goal is the development of automated techniques for the
formal verification of BPMN processes at design time, with a
especial focus on the key problem of resource allocation. We
provide a rewriting logic formalization of BPMN which enables the
automatic evaluation of several properties of interest on
processes, such as the resource usage over time and the usage
percentage for each resource replica. These properties can be
helpful for precisely identifying and optimizing the allocation of
resources in a process. The analysis is achieved by using the
rewriting-based Maude
tool.
The approach is illustrated with several examples, for which we
provide results on several experiments.
The Maude implementation of the algorithm and some example processes are available here. Check the README file for instructions on how to execute the test cases.
Several case studies are available:|
For further information, please, contact F. Dur�n,* G. Sala�n,* or C. Rocha* |