SBAT. A stochastic BPMN analysis tool

Luke Thomas Herbert, Zaza Nadja Lee Hansen, Peter Jacobsen

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


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.
Original languageEnglish
Title of host publicationProceedings of the ASME 2014 12th Biennial Conference on Engineering Systems Design and Analysis (ESDA 2014)
Number of pages10
PublisherAmerican Society of Mechanical Engineers
Publication date2014
ISBN (Print)978-0-7918-4585-1
Publication statusPublished - 2014
EventASME 2014 12th Biennial Conference on Engineering Systems Design and Analysis - Copenhagen, Denmark
Duration: 25 Jun 201427 Jun 2014
Conference number: 12


ConferenceASME 2014 12th Biennial Conference on Engineering Systems Design and Analysis
Internet address

Fingerprint Dive into the research topics of 'SBAT. A stochastic BPMN analysis tool'. Together they form a unique fingerprint.

Cite this