Formalizing and reasoning about the requirements specifications of workflow systems

This work addresses the problem of workflow requirements specifications con sidering 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 t he users to specify their requirements (and expectations) and test if the i nformation that they have provided is, in a sense, sufficient for the workf low to behave "as desired", in terms of the goal. Our methodology allows do main experts to express not only their knowledge, but also the "ignorance" (the semantics allows for unknown values to reflect a realistic situation o f agents dealing with incomplete information) and the possibility of occurr ence of exceptional situations. As a basis for formalizing the process of r equirements specifications, we are using the recent results on reasoning ab out actions. We propose a high level language Aw which enables specifying t he effects that activites have on the environment and how they should be co ordinated. We also describe our prototype tool for process specification. S trictly 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 relati on which enables reasoning about the correctness of the specification, in t erms of achieving a desired goal and, also testing about consequences of mo difications in the workflow descriptions.