We present a framework for modelling and analysis of real-world business workflows. Business processes regularly form the basis for the design of software services, and frequently display complex stochastic behaviour. The accurate evaluation of their qualitative aspects can allow for determining bounds on resources consumed during execution of business processes. Accurate resource provisioning is often central to ensuring the safe execution of a process. We first introduce a formalised core subset of the Business Process Modelling and Notation (BPMN), which we extend with probabilistic and non-deterministic branching and reward annotations. We then develop an algorithm for the efficient translation of these models into the guarded command language used by the model checker PRISM, in turn enabling model checking of BPMN processes and allowing for the calculation of a wide range of quantitative properties of business processes including transient probabilities, timing, occurrence and ordering of events, and best- and worst-case scenarios. The developments presented are illustrated using an example from the health-care industry.
High Assurance Systems Engineering, Ieee International Symposim on, 2012, p. 98-105
BPMN; Probabilistic BPMN; Stochastic Model Checking; Service Engineering; Quantitative Service Analysis; Service Provisioning
Main Research Area:
I E E E International Symposium on High-assurance Systems Engineering
14th IEEE International Symposium on High-Assurance Systems Engineering (HASE 2012)High Assurance Systems Engineering Symposium