Skip to main content

Property Specifications for Workflow Modelling

Peter Y.H. Wong and Jeremy Gibbons

Abstract

Previously we provided two formal behavioural semantics for Business Process Modelling Notation (BPMN) in the process algebra CSP. By exploiting CSP's refinement orderings, developers may formally compare their BPMN models. However, BPMN is not a specification language, and it is difficult and sometimes impossible to construct behavioural properties against which BPMN models may be verified. This paper considers a pattern-based approach for capturing these behavioural properties. We describe a property specification language PL for capturing a generalisation of Dwyer et al.'s Property Specification Patterns, and present a translation from PL into a bounded, positive fragment of linear temporal logic, which can then be automatically translated into CSP for simple refinement checking. We demonstrate its application via a simple example.

Book Title
Proceedings of 7th International Conference on Integrated Formal Methods
Month
February
Note
Invited for special issue in Science of Computer Programming. Technical report version available at http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/psp.pdf
Series
LNCS
Volume
5423
Year
2009