Formalising Workflow: A CCS-inspired Characterisation of the YAWL Workflow Patterns

摘要

We present work concerning the formal specification of business processes. It is of substantial benefit to be able to pin down the meaning of business processes precisely. This is an end in itself, but we are also concerned to do so in order that we might prove properties about the business processes that are being specified. It is a notable characteristic of most languages for representing business processes that they lack a robust semantics, and a notable characteristic of most commercial Business Process Management products that they have no support for verification of business process models. We define a high-level meta-model, called Liesbet, for representing business processes. The ontological commitments for Liesbet are sourced from the YAWL workflow patterns, which have been defined from studies into the behavioural nature of business processes. A formal characterisation of Liesbet is provided using Milner's Calculus of Communicating Systems (CCS). In this article, we omit some of the technical details of this characterisation and instead present the essential features by means of an abstract machine language, called LCCS. We also explain how we have facilitated the verification of certain properties of business processes specified in Liesbet, and discuss how Liesbet supports the YAWL workflow patterns. We include a simple three-part example of using Liesbet.