Abstract:
A fundamental requirement in specifying transaction systems is the need for a clear, concise, unambiguous, and rigorous behavioural and functional description of the systems' crucial features like concurrency, nondeterminism, mutual exclusion, synchronization, and deadlock avoidance. To write a specification that exhibits these characteristics requires a formalism that has both expressive power and the functionality for specifying and reasoning about the structure and behaviour of transaction models. To ensure that the specifications are consistent and verifiably correct requires expressing the specifications using mathematical notations and then using the notations' underlying formalism to prove correctness properties. Such requirements can only be satisfied within a formal framework. However, most of the present transaction systems (models) are not formally specified or at best use methodologies that are ad hoc or semiformal. Unfortunately, when insufficient formalism is used to specify transaction systems protocols they are open to different interpretations thereby violating the preservation of specification interpretations requirement. Therefore, there is need for a thorough modelling of the systems based on formal models that are easy to use, verify and validate. In this thesis, a Timed CSP based formal framework for transaction management is given. This framework is more general and not biased towards specific types of transaction. It integrates temporal behaviour of individual transactions with the dependencies among transactions that can arise e.g., when accessing shareable data objects. Further, the framework uses an event-based model based on causality and time because the partial orders together can naturally model concurrent events between transaction. In addition, the causality and time information are useful in analysing transaction execution for determining correctness and recoverable histories. In brief, this thesis provides a taxonomy of a transaction's specification characteristics against which any specification can be assessed; presents a suite of requirements for an adequate formalism in which various concurrent activities and interactions of transactions can be naturally expressed; provides record data type extensions to CSP; specifies transactions correctness criteria and concurrency control protocols; and presents an abstract level specification of an application, the Electronic Shopping Mall, to illustrate the concepts introduced.
