Login | Register

Modular composition and verification of transaction processing protocols using category theory

Title:

Modular composition and verification of transaction processing protocols using category theory

Janarthanan, Vasudevan (2003) Modular composition and verification of transaction processing protocols using category theory. Masters thesis, Concordia University.

[thumbnail of MQ77971.pdf]
Preview
Text (application/pdf)
MQ77971.pdf
5MB

Abstract

Establishing the correctness of reliable distributed protocols supporting dependable applications necessitates modular/compositional approaches to tackle the inherent complexity of these protocols. Efforts involved in the specification and verification of these reliable distributed protocols can be considerably reduced if the protocol is composed utilizing smaller components (building-blocks) possessing individual functionalities that are integral parts of the overall protocol operation. In this thesis, we introduce techniques utilizing the concepts of category theory for the modular composition of dependable distributed protocols. In particular, we show how by defining external interfaces of basic modules, and morphisms linking two different modules, a larger or more complex protocol can be formally composed and verified. To illustrate the effectiveness of the proposed methodology for compositional specification and verification, in this thesis, we present a modular composition and verification of a transaction processing protocol namely the non-blocking atomic three phase commit (3PC) protocol using category theoretic concepts. Specifically, we illustrate how the overall global properties of the protocol can be proved by utilizing constructs of local sub-properties of the inherent building blocks of the 3PC protocol. A key benefit of this modular approach is that these identified building blocks would be helpful to system designers for their capability of specifying and facilitating rigorously tested and pretested formal theory modules of required system and component behavior; and also supporting system design decisions and modifications.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Janarthanan, Vasudevan
Pagination:xiv, 172 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Date:2003
Thesis Supervisor(s):Sinha, Purnendu
Identification Number:QA 76.9 M3J36 2003
ID Code:1923
Deposited By: Concordia University Library
Deposited On:27 Aug 2009 17:23
Last Modified:13 Jul 2020 19:50
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top