| Serializability is the correctness criterion generally used in the literature to determine a schedule's correctness. Such a criterion is clearly inappropriate, however, in determining the correctness of schedules that are produced when an application is run at an isolation level lower than SERIALIZABLE since such schedules might no longer be serializable. In this dissertation, using semantic-correctness criterion, we prove a condition for each isolation level under which transactions that execute at that level will be semantically correct.; We also apply the semantic-correctness theory to automatic workflow verification and generation problems. In particular, we propose a new workflow model that allows one to: (1) automatically check if the desired outcome of a workflow can be produced by its actual implementation, (2) automatically synthesize a workflow implementation from a workflow specification and a given task library. Finally, we present several preliminary theoretical results for the completeness of a task library and the realizability of a workflow postcondition. |
