Open AccessProperty Specifications for Workflow Modelling
Author(s) -
Peter Y. H. Wong,
Jeremy Gibbons
Publication year - 2009
Publication title -
lecture notes in computer science
Language(s) - English
Resource type - Book series
SCImago Journal Rank - 0.249
H-Index - 400
eISSN - 1611-3349
pISSN - 0302-9743
DOI - 10.1007/978-3-642-00255-7_5
Subject(s) - computer science , business process model and notation , programming language , fragment (logic) , workflow , notation , semantics (computer science) , property (philosophy) , formal specification , model checking , process calculus , xpdl , principle of compositionality , theoretical computer science , business process , business process modeling , artificial intelligence , database , workflow technology , work in process , mathematics , philosophy , arithmetic , epistemology , marketing , business
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 PL for capturing a generalisation 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. We demonstrate its application via a simple example
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom