Formalisations and applications of BPMN
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...
Auteurs principaux: | , |
---|---|
Format: | Journal article |
Langue: | English |
Publié: |
2011
|
_version_ | 1826257015870062592 |
---|---|
author | Wong, P Gibbons, J |
author_facet | Wong, P Gibbons, J |
author_sort | Wong, P |
collection | OXFORD |
description | 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. © 2009 Elsevier B.V. All rights reserved. |
first_indexed | 2024-03-06T18:11:26Z |
format | Journal article |
id | oxford-uuid:032c9898-3bd5-4ee4-905e-d5ff7dab00d8 |
institution | University of Oxford |
language | English |
last_indexed | 2024-03-06T18:11:26Z |
publishDate | 2011 |
record_format | dspace |
spelling | oxford-uuid:032c9898-3bd5-4ee4-905e-d5ff7dab00d82022-03-26T08:44:30ZFormalisations and applications of BPMNJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:032c9898-3bd5-4ee4-905e-d5ff7dab00d8EnglishSymplectic Elements at Oxford2011Wong, PGibbons, JWe 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. © 2009 Elsevier B.V. All rights reserved. |
spellingShingle | Wong, P Gibbons, J Formalisations and applications of BPMN |
title | Formalisations and applications of BPMN |
title_full | Formalisations and applications of BPMN |
title_fullStr | Formalisations and applications of BPMN |
title_full_unstemmed | Formalisations and applications of BPMN |
title_short | Formalisations and applications of BPMN |
title_sort | formalisations and applications of bpmn |
work_keys_str_mv | AT wongp formalisationsandapplicationsofbpmn AT gibbonsj formalisationsandapplicationsofbpmn |