Property Specifications for Workflow Modelling
Peter Y.H. Wong and Jeremy Gibbons
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.
Proceedings of 7th International Conference on Integrated Formal Methods
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