Projects per year
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.
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 language | English |
---|
Place of Publication | Kgs. Lyngby |
---|---|
Publisher | Technical University of Denmark |
Number of pages | 300 |
Publication status | Published - 2014 |
Series | DTU Compute PHD-2014 |
---|---|
Number | 303 |
ISSN | 0909-3192 |
Bibliographical note
The work presented in this thesis was jointly funded by Intelligent Hospital Systems and the Technical University of Denmark.Fingerprint
Dive into the research topics of 'Specification, Verification and Optimisation of Business Processes: A Unified Framework'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Specifying and verifying medical robotics software to ensure harmless operation
Herbert, L. T., Hansen, M. R., Kindler, E., Fränzle, M., Weske, M. & Sharp, R.
Technical University of Denmark
01/03/2010 → 24/06/2014
Project: PhD