Specification, Verification and Optimisation of Business Processes

A Unified Framework

Luke Thomas Herbert

Research output: Book/ReportPh.D. thesis

965 Downloads (Pure)

Abstract

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
Number303
ISSN0909-3192

Bibliographical note

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

Cite this

Herbert, L. T. (2014). Specification, Verification and Optimisation of Business Processes: A Unified Framework. Kgs. Lyngby: Technical University of Denmark. DTU Compute PHD-2014, No. 303
Herbert, Luke Thomas. / Specification, Verification and Optimisation of Business Processes : A Unified Framework. Kgs. Lyngby : Technical University of Denmark, 2014. 300 p. (DTU Compute PHD-2014; No. 303).
@phdthesis{f9069d591114456f868509805052b271,
title = "Specification, Verification and Optimisation of Business Processes: A Unified Framework",
abstract = "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.",
author = "Herbert, {Luke Thomas}",
note = "The work presented in this thesis was jointly funded by Intelligent Hospital Systems and the Technical University of Denmark.",
year = "2014",
language = "English",
publisher = "Technical University of Denmark",

}

Herbert, LT 2014, Specification, Verification and Optimisation of Business Processes: A Unified Framework. DTU Compute PHD-2014, no. 303, Technical University of Denmark, Kgs. Lyngby.

Specification, Verification and Optimisation of Business Processes : A Unified Framework. / Herbert, Luke Thomas.

Kgs. Lyngby : Technical University of Denmark, 2014. 300 p. (DTU Compute PHD-2014; No. 303).

Research output: Book/ReportPh.D. thesis

TY - BOOK

T1 - Specification, Verification and Optimisation of Business Processes

T2 - A Unified Framework

AU - Herbert, Luke Thomas

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

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

M3 - Ph.D. thesis

BT - Specification, Verification and Optimisation of Business Processes

PB - Technical University of Denmark

CY - Kgs. Lyngby

ER -

Herbert LT. Specification, Verification and Optimisation of Business Processes: A Unified Framework. Kgs. Lyngby: Technical University of Denmark, 2014. 300 p. (DTU Compute PHD-2014; No. 303).