Master's Research (MASc)

 

 

 

 

 

 

 

     Research Interests:

  • Distributed Systems

  • Embedded Systems

  • Real-Time Systems

  • Category Theory

  • Formal Methods

  • Real-Time Protocols

  • Theoretical Computer Science

 

     Research Project:

  • Modular Composition and Verification of Three Phase Commit Protocol Using Category Theory

      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 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 my research work, I utilized the concepts of category theory for modular composition of dependable distributed protocols. In particular, I showed that by defining external interfaces of basic modules, and morphisms linking two different modules, a larger or more complex protocol could be formally composed and verified in a much simpler way. For this purpose, I considered a transaction processing protocol namely the non-blocking atomic three phase commit (3PC) protocol to 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.