• Libraries
    • Log in to:
    View Item 
    •   MSpace Home
    • Faculty of Graduate Studies (Electronic Theses and Practica)
    • FGS - Electronic Theses and Practica
    • View Item
    •   MSpace Home
    • Faculty of Graduate Studies (Electronic Theses and Practica)
    • FGS - Electronic Theses and Practica
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Specification of transaction systems protocols

    Thumbnail
    View/Open
    nq23597.pdf (12.20Mb)
    Date
    1997-05-01
    Author
    Ehikioya, Sylvanus Agbonifoh
    Metadata
    Show full item record
    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.
    URI
    http://hdl.handle.net/1993/878
    Collections
    • FGS - Electronic Theses and Practica [25061]

    DSpace software copyright © 2002-2016  DuraSpace
    Contact Us | Send Feedback
    Theme by 
    Atmire NV
     

     

    Browse

    All of MSpaceCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    My Account

    Login

    Statistics

    View Usage Statistics

    DSpace software copyright © 2002-2016  DuraSpace
    Contact Us | Send Feedback
    Theme by 
    Atmire NV