Verification of Correctness and Data-Flow Properties for Workflow Processes in Maude

A business process is composed of interrelated tasks, executed inside an organization in order to accomplish a specific business goal. A workflow is the automation of a business process that can be executed by an information system. Besides the tasks (which constitute the control-flow level), the process also involves data information (which constitutes the data-flow level). The correctness of the processes is critical for ensuring the business goals and should be achieved both at the control-flow and at the data-flow level. In this paper we use Workflow Nets with Data for modelling the workflow processes with data and we propose the specification of Workflow Nets with Data as rewrite theories in the rewriting logic based language Maude. This approach will permit the use of model checking techniques to verify the correctness of the workflows, detect various data-flow anomalies and verify specific properties at the data-flow level.