Formalisations and applications of BPMN |
| |
Authors: | Peter Y.H. Wong Jeremy Gibbons |
| |
Affiliation: | Computing Laboratory, University of Oxford, United Kingdom |
| |
Abstract: | We present two formalisations of the Business Process Modelling Notation (BPMN). In particular, we introduce a semantic model for BPMN in the process algebra CSP; we then study an augmentation of this model in which we introduce relative timing information, allowing one to specify timing constraints on concurrent activities. By exploiting CSP refinement, we are able to show some relationships between the timed and the untimed models. We then describe a novel empirical studies’ model, and the transformation to BPMN, allowing one to apply our formal semantics for analysing different kinds of workflows. To provide a better facility for describing behaviour specification about a BPMN diagram, we also present a pattern-based approach using which a workflow designer could specify properties which could otherwise be difficult to express. Our approach is specifically designed to allow behavioural properties of BPMN diagrams to be mechanically verified via automatic model checking as provided by the FDR tool. We use two examples to illustrate our approach. |
| |
Keywords: | Business process CSP Model checking Property specifications Refinement Semantics Timed behaviour Workflow |
本文献已被 ScienceDirect 等数据库收录! |
|