Cookies on this website

We use cookies to ensure that we give you the best experience on our website. If you click 'Accept all cookies' we'll assume that you are happy to receive all cookies and you won't see this message again. If you click 'Reject all non-essential cookies' only necessary cookies providing core functionality such as security, network management, and accessibility will be enabled. Click 'Find out more' for information on how to change your cookie settings.

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. © 2010 IEEE.

Original publication




Journal article


Proceedings - 2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010

Publication Date



25 - 34