Formalizing and reasoning about the requirements specifications of workflow systems

This work addresses the problem of workflow requirements specifications considering the realistic assumptions that, it involves experts from different domains (i.e. representatives of different business policies); not all the possible execution scenarios are known beforehand, during the early stage of specification. In particular, since the main purpose of a workflow is to achieve a certain (bussiness) goal, we propose a formalism which enables the users to specify their requirements (and expectations) and test if the information that they have provided is, in a sense, sufficient for the workflow to behave "as desired", in terms of the goal. Our methodology allows domain experts to express not only their knowledge, but also the "ignorance" (the semantics allows for unknown values to reflect a realistic situation of agents dealing with incomplete information) and the possibility of occurrence of exceptional situations. As a basis for formalizing the process of requirements specifications, we are using the recent results on reasoning about actions. We propose a high level language A_W which enables specifying the effects that activites have on the environment and how they should be coordinated. We also describe our prototype tool for process specification. Strictly speaking, in this work we go "one step" before actual analysis and design, and offer a formalism which enables the involved partners to see if the extent to which they have expressed their domain knowledge (which may sometimes be subject to a proprietary restricions) can satisfy the intended needs and behaviour of their product_to_be. We define an entailment relation which enables reasoning about the correctness of the specification, in terms of achieving a desired goal and, also testing about consequences of modifications in the workflow descriptions.