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

Description complète

Détails bibliographiques
Auteurs principaux: Wong, P, Gibbons, J
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