Specification, Verification and Optimisation of Business Processes: A Unified Framework

Luke Thomas Herbert

Research output: Book/ReportPh.D. thesis

1492 Downloads (Pure)


This thesis develops a unified framework wherein to specify, verify and optimise stochastic business processes.

This framework provides for the modelling of business processes via a mathematical structure which captures business processes as a series of connected activities. This structure is extended with stochastic branching, message passing and reward annotations which allow for the modelling of resources consumed during the execution of a business process. Further, it is shown how this structure can be used to formalise the established business process modelling language Business Process Model and Notation (BPMN).

The automated analysis of business processes is done by means of quantitative probabilistic model checking which allows verification of validation and performance properties through use of an algorithm for the translation of business process models into a format amenable to model checking. This allows for a rich set of both qualitative and quantitative properties of a business process to be precisely determined in an automated fashion directly from the model of the business process.

A number of advanced applications of this framework are presented which allow for automated fault tree analysis and the automated optimisation of business processes by means of an evolutionary algorithm.

This work is motivated by problems that stem from the healthcare sector, and examples encountered in this field are used to illustrate these developments.
Original languageEnglish
Place of PublicationKgs. Lyngby
PublisherTechnical University of Denmark
Number of pages300
Publication statusPublished - 2014
SeriesDTU Compute PHD-2014

Bibliographical note

The work presented in this thesis was jointly funded by Intelligent Hospital Systems and the Technical University of Denmark.


Dive into the research topics of 'Specification, Verification and Optimisation of Business Processes: A Unified Framework'. Together they form a unique fingerprint.

Cite this