Model Checking BPMN, Property Specifications and Observation Workflow Model (OWorkflow)

This page contains information about two formal semantics for Business Process Modelling Notation (BPMN) in the process algebra CSP, property specifications for BPMN and the workflow model OWorkflow.

Model Checking BPMN

Modelling of business processes and workflows is an important area in software engineering. BPMN allows developers to take a process-oriented approach to modelling of systems. We have defined two semantic models (an untimed process semantics and a relative timed semantics) for this notation over the domain CSP. These semantic models allow BPMN diagrams to be formally analysed and compared. In particular, verifications can now be carried out against properties such as consistency and compatibility between business processes specified in BPMN via the FDR tool. This page contains a prototypical Haskell implementation of the semantic functions from BPMN to machine-readable CSP.


OWorkflow is designed for constructing specifications of long running empirical studies such as clinical trials in which observations for gathering data are performed at strict specific times. These observations, either manually performed or automated, are often interleaved with scientific procedures, and their descriptions are recorded in a calendar for scheduling and monitoring to ensure each observation is carried out correctly at a specific time. This page contains information about the Haskell implementation of the bidirectional transformation between OWorkflow and a subset of BPMN, by which graphical specification, simulation, automation and formalisation are made possible.

Property Specification for BPMN

While by exploiting CSP's refinement orderings business process developers may formally compare their BPMN models. BPMN is not a specification language and it is difficult and sometime impossible to construct behavioural properties against which BPMN models may be verified. This paper consider a pattern-based approach for capturing these behavioural properties. We have defined a property specification language PL for capturing a generalisation of Dwyer et al.'s Property Specification Patterns and a corresponding translation from PL into a bounded, positive fragment of linear temporal logic, which can then be automatically translated into CSP specification for simple refinement checking.

Source Code




        From BPMN to OWorkflow

        From OWorkflow to BPMN

        From BPMN to CSPM (purely untimed) (SOURCE1 [F= SOURCE2)

        From BPMN to CSPM (SOURCE1 [F= SOURCE2)

        From PL to CSPM (purely untimed) (SOURCE1 |= PL)

        From PL to CSPM (SOURCE1 |= PL)


A Process Semantics for BPMN.

Peter Y.H. Wong, Jeremy Gibbons

In Proceedings of 10th International Conference on Formal Engineering Methods. Vol. 5256 of LNCS. October 2008.

Extended version available at http://www.comlab.ox.ac.uk/peter.wong/pub/bpmnsem.pdf.

Verifying Business Process Compatibility.

Peter Y.H. Wong, Jeremy Gibbons

In Proceedings of 8th International Conference on Quality Software. IEEE Computer Society. August 2008.

Preliminary versions were presented at 3rd International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems and 2nd European Young Researchers Workshop on Service Oriented Computing, June 2007.

A Relative Timed Semantics for BPMN.

Peter Y.H. Wong, Jeremy Gibbons

In Proceedings of 7th International Workshop on the Foundations of Coordination Languages and Software Architectures. ENTCS. July 2008.

Invited for special issue in Science of Computer Programming. A shorter version of this paper was presented at the 3rd European Young Researchers Workshop on Service Oriented Computing, London, United Kingdom, June 2008. Extended version available at http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/bpmntime.pdf.

On Specifying and Visualising Long-Running Empirical Studies.

Peter Y.H. Wong, Jeremy Gibbons

In Proceedings of International Conference on Model Transformation. Vol. 5063 of LNCS. July 2008.

Extended version available at http://www.comlab.ox.ac.uk/peter.wong/pub/transext.pdf.

Property Specifications for Workflow Modelling.

Peter Y.H. Wong, Jeremy Gibbons

In Proceedings of 7th International Conference on Intergrated Formal Methods. Vol. 5423 of LNCS. Feb 2009.

Technical report version available at http://www.comlab.ox.ac.uk/peter.wong/pub/psp.pdf.


For any enquiries please email peter (dot) wong (at sign) comlab (dot) ox (dot) ac (dot) uk.


Other research and teaching information can be found from my main page.

Random Image
Random Image
Random Image