Breadcrumb

 
 

A modular approach to formal specification and verification of dependable distributed protocols

Title:

A modular approach to formal specification and verification of dependable distributed protocols

Ren, Da Qi (2002) A modular approach to formal specification and verification of dependable distributed protocols. Masters thesis, Concordia University.

[img]
Preview
PDF
3393Kb

Abstract

Dependable distributed system typically utilize a hierarchy of protocols to provide for reliable and timely services. Such protocols have both dependability and real-time attributes, and the analysis of these protocols is a problem of growing complexity. The development of precise and accurate formal specifications of these protocols and their subsequent formal verification to gain assurance have been a great challenge. Exploiting the inherent modularity in the design of most dependable protocols, in this thesis, we present our modular approach to specification composition and verification of dependable distributed protocol. In particular, we consider redundancy management protocols that are needed to manage redundant resources used in the system for dependability purposes. Utilizing building-block protocols inherently used in redundancy management protocols, we perform compositional specification and verification of a checkpointing and recovery protocol based on them. The key idea is that if a library of these basic components, like the primitives and sub-protocols are being formulated, then these elements aid in systematic and hierarchical development of dependable distributed protocols. The main contribution of this thesis to illustrate the fact that by defining a priori validated building-blocks for dependable distributed protocols, larger and more complex protocols can be easily specified and verified. For a mechanical support in formal verification process, we use formal tools such as Specware and PVS.

Divisions:Concordia University > Faculty of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Ren, Da Qi
Pagination:ix, 97 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:Theses (M.A.Sc.)
Program:Electrical and Computer Engineering
Date:2002
Thesis Supervisor(s):Sinha, Purnendu
ID Code:1870
Deposited By:Concordia University Libraries
Deposited On:27 Aug 2009 13:23
Last Modified:08 Dec 2010 10:23
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

Document Downloads

More statistics for this item...

Concordia University - Footer