Show simple item record

dc.contributor.author Ehikioya, Sylvanus Agbonifoh en_US
dc.date.accessioned 2007-05-15T15:20:01Z
dc.date.available 2007-05-15T15:20:01Z
dc.date.issued 1997-05-01T00:00:00Z en_US
dc.identifier.uri http://hdl.handle.net/1993/878
dc.description.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. en_US
dc.format.extent 12800013 bytes
dc.format.extent 184 bytes
dc.format.mimetype application/pdf
dc.format.mimetype text/plain
dc.language en en_US
dc.language.iso en_US
dc.title Specification of transaction systems protocols en_US
dc.degree.discipline Computer Science en_US
dc.degree.level Doctor of Philosophy (Ph.D.) en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

View Statistics