Abstract
This paper presents SBAT, a tool framework for the modelling and analysis of complex business workflows. SBAT is applied to analyse an example from the Danish baked goods industry.
Based upon the Business Process Modelling and Notation (BPMN) language for business process modelling, we describe a formalised variant of this language extended to support the addition of intention preserving stochastic branching and parameterised reward annotations. Building on previous work, we detail the design of SBAT, a software tool which allows for the analysis of BPMN models. Within SBAT, properties of interest are specified using the temporal logic Probabilistic Computation Tree Logic (PCTL) and we employ stochastic model checking, by means of the model checker PRISM, to compute their exact values.
We present a simplified example of a distributed stochastic system where we determine a reachability property and the value of associated rewards in states of interest for a real-world example from a case company in the Danish baked goods industry. The developments are presented in a generalised fashion to make them relevant to the general problem of implementing quantitative probabilistic model checking of graph-based process modelling languages.
This paper contains three key elements:
1. SBAT description.
2. Case company description.
3. Using SBAT on the case company.
The paper concludes by indicating SBAT’s practical applicability and suggests further research directions.
Based upon the Business Process Modelling and Notation (BPMN) language for business process modelling, we describe a formalised variant of this language extended to support the addition of intention preserving stochastic branching and parameterised reward annotations. Building on previous work, we detail the design of SBAT, a software tool which allows for the analysis of BPMN models. Within SBAT, properties of interest are specified using the temporal logic Probabilistic Computation Tree Logic (PCTL) and we employ stochastic model checking, by means of the model checker PRISM, to compute their exact values.
We present a simplified example of a distributed stochastic system where we determine a reachability property and the value of associated rewards in states of interest for a real-world example from a case company in the Danish baked goods industry. The developments are presented in a generalised fashion to make them relevant to the general problem of implementing quantitative probabilistic model checking of graph-based process modelling languages.
This paper contains three key elements:
1. SBAT description.
2. Case company description.
3. Using SBAT on the case company.
The paper concludes by indicating SBAT’s practical applicability and suggests further research directions.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the ASME 2014 12th Biennial Conference on Engineering Systems Design and Analysis (ESDA 2014) |
| Number of pages | 10 |
| Volume | 3 |
| Publisher | The American Society of Mechanical Engineers (ASME) |
| Publication date | 2014 |
| ISBN (Print) | 978-0-7918-4585-1 |
| DOIs | |
| Publication status | Published - 2014 |
| Event | ASME 2014 12th Biennial Conference on Engineering Systems Design and Analysis - Copenhagen, Denmark Duration: 25 Jun 2014 → 27 Jun 2014 Conference number: 12 http://www.asmeconferences.org/ESDA2014/ |
Conference
| Conference | ASME 2014 12th Biennial Conference on Engineering Systems Design and Analysis |
|---|---|
| Number | 12 |
| Country/Territory | Denmark |
| City | Copenhagen |
| Period | 25/06/2014 → 27/06/2014 |
| Internet address |