Specification of transaction systems protocols

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...

Full description

Bibliographic Details
Main Author: Ehikioya, Sylvanus Agbonifoh
Language:en_US
Published: 2007
Online Access:http://hdl.handle.net/1993/878
id ndltd-MANITOBA-oai-mspace.lib.umanitoba.ca-1993-878
record_format oai_dc
spelling ndltd-MANITOBA-oai-mspace.lib.umanitoba.ca-1993-8782014-01-31T03:30:18Z Specification of transaction systems protocols Ehikioya, Sylvanus Agbonifoh 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. 2007-05-15T15:20:01Z 2007-05-15T15:20:01Z 1997-05-01T00:00:00Z http://hdl.handle.net/1993/878 en_US
collection NDLTD
language en_US
sources NDLTD
description 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.
author Ehikioya, Sylvanus Agbonifoh
spellingShingle Ehikioya, Sylvanus Agbonifoh
Specification of transaction systems protocols
author_facet Ehikioya, Sylvanus Agbonifoh
author_sort Ehikioya, Sylvanus Agbonifoh
title Specification of transaction systems protocols
title_short Specification of transaction systems protocols
title_full Specification of transaction systems protocols
title_fullStr Specification of transaction systems protocols
title_full_unstemmed Specification of transaction systems protocols
title_sort specification of transaction systems protocols
publishDate 2007
url http://hdl.handle.net/1993/878
work_keys_str_mv AT ehikioyasylvanusagbonifoh specificationoftransactionsystemsprotocols
_version_ 1716628132858953728