Property specifications for workflow modelling

Previously we provided two formal behavioural semantics for the 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 use it to construct behavioural properties against which other BPMN models may be verified. This paper considers a pattern-based approach to expressing behavioural properties. We describe a property specification language PLPL for capturing a generalisation of Dwyer et al.’s Property Specification Patterns, and present a translation from PLPL into a bounded, positive fragment of linear temporal logic, which can then be automatically translated into CSP for simple refinement checking. We present a detailed example studying the behavioural properties of an airline ticket reservation business process. Using the same example we also describe some recent results on expressing behavioural compatibility within our semantic models. These results lead to a compositional approach for ensuring deadlock freedom of interacting business processes.

Research highlights
► A small specification language PL for behavioural property specification of workflows.
► Automatic verification of workflows against PL terms.
► A usable property specification technique accessible to workflow designers/analysts.
► A compositional approach to ensuring deadlock-freedom of interacting workflows.