Ren, Da Qi (2002) A modular approach to formal specification and verification of dependable distributed protocols. Masters thesis, Concordia University.
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.|
|Degree Name:||Theses (M.A.Sc.)|
|Program:||Electrical and Computer Engineering|
|Thesis Supervisor(s):||Sinha, Purnendu|
|Deposited By:||Concordia University Libraries|
|Deposited On:||27 Aug 2009 13:23|
|Last Modified:||08 Dec 2010 10:23|
Repository Staff Only: item control page