| A workflow is a collection of cooperating, coordinated activities designed to carry out a well-defined complex process, such as trip planning, graduate student registration procedure, or a business process in a large enterprise. Executing a workflow, thus, involves coordinated execution of multiple long-running steps in an environment of distributed, heterogeneous processing entities. Workflow management systems provide a framework for capturing the interaction among the activities in a workflow and are recognized as a new paradigm for integrating disparate systems, including legacy systems. However, in order to realize its full potential a number of limitations of the current workflow models, including lack of a clear theoretical basis has to be addressed. Workflows must be specified declaratively, verified formally, and scheduled automatically. In this dissertation first we show that Concurrent Transaction Logic (abbr. CTR) is a natural logical formalism for representing workflow control graphs, temporal and causality constraints that workflow executions must obey, for reasoning about the consistency of workflow specifications, and for scheduling workflows in the presence of those constraints. Next, we develop Game-CTR, a natural extension of CTR designed for modeling and reasoning about run-time properties of workflows that are composed of non-cooperating services—such as Web services. We develop a model and proof theory for Game-CTR and show how it can be used to specify executions under a fairly large class of temporal and causality constraints. We then develop a game solver algorithm that converts such specifications (which are formulas in Game-CTR) into other, equivalent Game-CTR formulas, a coordinator, that can be executed more efficiently and without backtracking. |
