A Guarded Workflow Language and Its Formal Semantics

Many information systems hold data of considerable value, and are subject to complex constraints and business rules. In these systems, update operations are often carefully described, to the extent that it is possible to derive a formal specification of their applicability and effect. Where an update is performed by means of a workflow, as a combination of operations, then it may be advantageous to calculate properties of that workflow from the specifications of the operations involved. This paper introduces a formal notation for the description and analysis of workflows, similar to the well-known languages of guarded commands or generalised substitutions. This notation is given a behavioural semantics corresponding to a sequential, transformational view of the information system. This semantics can then be used to determine the suitability of proposed guards-constraints upon the enactment of workflows-and to establish whether one workflow will interfere with the progress of another.