Abstract
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.
Original language | English |
---|---|
Title of host publication | 2012 IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE) |
Publisher | IEEE |
Publication date | 2012 |
Pages | 98-105 |
ISBN (Print) | 978-1-4673-4742-6 |
DOIs | |
Publication status | Published - 2012 |
Event | 2012 IEEE 14th International Symposium on High-Assurance Systems Engineering - Omaha, United States Duration: 25 Oct 2012 → 27 Oct 2012 Conference number: 14 https://ieeexplore.ieee.org/xpl/conhome/6374352/proceeding |
Conference
Conference | 2012 IEEE 14th International Symposium on High-Assurance Systems Engineering |
---|---|
Number | 14 |
Country/Territory | United States |
City | Omaha |
Period | 25/10/2012 → 27/10/2012 |
Internet address |
Series | I E E E International Symposium on High-Assurance Systems Engineering |
---|---|
ISSN | 1530-2059 |
Keywords
- BPMN
- Probabilistic BPMN
- Stochastic Model Checking
- Service Engineering
- Quantitative Service Analysis
- Service Provisioning