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 use it to construct behavioural properties against which BPMN models may be verified. This paper considers a pattern-based approach to expressing 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: Proceedings of the 21st International Conference on Software Engineering (1999)
Formal Systems (Europe) Ltd. Failures-Divergences Refinement, FDR2 User Manual (1998), http://www.fsel.com
Lowe, G.: Specification of communicating processes: temporal logic versus refusals-based refinement. Formal Aspects of Computing 20(3) (2008)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)
Mukarram, A.: A Refusal Testing Model for CSP. D.Phil thesis, University of Oxford (1992)
Object Management Group. BPMN Specification (February 2006), http://www.bpmn.org
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)
Wong, P.Y.H., Gibbons, J.: A Process Semantics for BPMN. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 355–374. Springer, Heidelberg (2008), http://www.comlab.ox.ac.uk/peter.wong/pub/bpmnsem.pdf
Wong, P.Y.H., Gibbons, J.: A Relative-Timed Semantics for BPMN. In: Proceedings of 7th International Workshop on the Foundations of Coordination Languages and Software Architectures, July 2008. ENTCS (2008); Invited for special issue in Science of Computer Programming, http://www.comlab.ox.ac.uk/peter.wong/pub/foclasa08.pdf
Wong, P.Y.H., Gibbons, J.: Property Specifications for Workflow Modelling. Technical Report, University of Oxford (2008), http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/psp.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wong, P.Y.H., Gibbons, J. (2009). Property Specifications for Workflow Modelling. In: Leuschel, M., Wehrheim, H. (eds) Integrated Formal Methods. IFM 2009. Lecture Notes in Computer Science, vol 5423. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00255-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-00255-7_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00254-0
Online ISBN: 978-3-642-00255-7
eBook Packages: Computer ScienceComputer Science (R0)