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

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.