Property Specifications for Workflow Modelling
Previously the authors provided two formal behavioral semantics for Business Process Modeling 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 behavioral properties against which BPMN models may be verified. This paper considers a pattern-based approach for capturing these behavioral properties. They describe a property specification language PL for capturing a generalization 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. They demonstrate its application via a simple example.