@inproceedings{pattern,
  abstract = "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 <em>PL</em> for capturing a generalisation of Dwyer et al.'s Property Specification Patterns, and present a translation from <em>PL</em> 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.",
  author = "Peter Y.H. Wong and Jeremy Gibbons",
  booktitle = "Proceedings of 7th International Conference on Integrated Formal Methods",
  doi = "10.1007/978-3-642-00255-7_5",
  month = "February",
  note = "Invited for special issue in Science of Computer Programming. Technical report version available at \url{http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/psp.pdf}",
  series = "LNCS",
  title = "Property Specifications for Workflow Modelling",
  volume = "5423",
  year = "2009",
}