SBOAT: A Stochastic BPMN Analysis and Optimisation Tool

In this paper we present a description of a tool development framework, called SBOAT, for the quantitative analysis of graph based process modelling languages based upon the Business Process Modelling and Notation (BPMN) language, extended with intention preserving stochastic branching and parameterised reward annotations.

SBOAT allows the optimisation of these processes by specifying optimisation goals by means of probabilistic control tree logic (PCTL). Optimisation is performed by means of an evolutionary algorithm where stochastic model checking, in the form of the PRISM model checker, is used to compute the fitness, the performance of a candidate in terms of the specified goals, of variants of a process.

Our evolutionary algorithm approach uses a matrix representation of process models to efficiently allow mutation and crossover of a process model to be performed, allowing broad exploration of the space of possible models. We present a simple example of a distributed stochastic system where we determine a reachability property and the value of associated rewards in states of interest for a generated range of models.

This example is taken from a case company in the Danish baking industry and will illustrate the practical applicability of this tool by helping the company analyse and optimise selected workflows.