BPMN

This page contains information about:

• 1. Formalisations of Business Process Modelling Notation (BPMN) using the process algebra CSP;

  2. Property specifications method for BPMN;

  3. Applications to business process and empirical studies modelling.

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.

Empirical Studies

We have developed a declarative model Empiricol 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 this model 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

to be added...

Requirements

• • Compiling Haskell: GHC 6.4.2 or above

  • Parsing XML: HaXml-1.13.3

  • Editing BPMN: ILOG JViews BPMN Modeler

  • Model checking CSP: FDR tool (requires support for the refusal traces model if using specification language PL)

Manual

to be added...

Literatures

Doctorate (DPhil) Thesis

• 1. Formalisations and Applications of Business Process Modelling Notation. DPhil Thesis, Department of Computer Science, University of Oxford, 2011.

Journal Publications

• 1. P.Y.H. Wong and J. Gibbons, Formalisations and Applications of BPMN. Special issue of FOCLASA08, volume 76, issue 8 of Science of Computer Programming, Aug 2011. DOI (10.1016/j.scico.2009.09.010).

  2. P.Y.H. Wong and J. Gibbons, Property Specifications for Workflow Modelling. Special issue of IFM2009, volume 76, issue 10 of Science of Computer Programming, Oct 2011. DOI (10.1016/j.scico.2010.09.007).

Conference and Workshop Publications

• 1. P.Y.H. Wong and J. Gibbons, Property Specifications for Workflow Modelling. In Proceedings of 7th International Conference on Integrated Formal Methods, volume 5423 of LNCS, Dusseldof, Germany. Feb 2009. Invited for special issue in Science of Computer Programming. DOI (10.1007/978-3-642-00255-7_5). (Extended version)

  2. P.Y.H. Wong and J. Gibbons, A Process Semantics for BPMN. In Proceedings of 10th International Conference on Formal Engineering Methods, volume 5256 of LNCS, Kitakyushu (Kokura), Japan. Oct 2008. DOI (10.1007/978-3-540-88194-0_22). (Extended version)

  3. P.Y.H. Wong and J. Gibbons, Verifying Business Process Compatibility. In Proceedings of 8th International Conference on Quality Software, IEEE Computer Society, Oxford, UK. Aug 2008. DOI (10.1109/QSIC.2008.6)

  4. P.Y.H. Wong and J. Gibbons, A Relative Timed Semantics for BPMN. In Proceedings of 7th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA08), ENTCS, Reykjavik, Iceland. Jul 2008. Accepted for special issue in Science of Computer Programming. DOI(10.1016/j.entcs.2009.06.029). (Extended version)

  5. P.Y.H. Wong and J. Gibbons, On Specifying and Visualising Long-Running Empirical Studies. In Proceedings of International Conference on Model Transformations, volume 5063 of LNCS, Zurich, Switzerland. Jul 2008. DOI (10.1007/978-3-540-69927-9_6). (Extended version)