Formal tools for specification-driven protocol design of distributed computing systems

Abstract

The widespread use of Distributed Computing Systems (DCSs) is due to the advantages of better performance, improved reliability, efficient resource sharing and easy upgradability. In order to realize the advantages of a DCS, many issues associated with their design should be tackled efficiently. One such significant issue is the design and development of a protocol and same is the theme of this thesis. The development of a protocol typically consists of studies related to its design, specification, validation and performance evaluation. The research in the area of protocols has been mainly concentrated on the specification and validation aspects. Many techniques have been proposed for these two aspects. But prior to the initiation of the actions of specification and validation of the protocol, the protocol should be designed systematically. Not much research work has been reported in this area. In view of this, an effort has been made in this thesis to develop a systematic procedure for designing protocols for a DCS, starting from the specifications of a DCS and the protocol requirements. The design and development of a protocol can be divided into six phases: (i) specification of the DCS, (ii) specification of protocol requirements, (iii) protocol design, (iv) specification and validation of the designed protocol, (v) performance evaluation and (vi) hardware/ software implementation. In this thesis a formal method based on matrix and set theoretic concepts has been developed for the specification of a DCS keeping in view the protocol design aspects. The DCS is characterized by various properties such as concurrency, strong concurrency, exclusiveness and sequencing. A 6-tuple model is presented to specify a DCS and methods are given to compute these properties of the DCS from this model. The technique presented for the specification of a DCS has many advantages as compared to other existing techniques of specification. Further, inconsistencies of specification and deadlock caused due to improper specification can easily be detected using this technique. A similar technique is developed for the specification of protocol requirements. These two formal specification techniques form the basis of the development of simple and straightforward procedures for the design of the protocol. The applicability of the above design procedure has been illustrated by considering an example of a computing system encountered onboard a spacecraft. A Petri net based approach has been adopted to model the protocol. New methods are developed to compute the invariants of Petri nets and colored Petri nets. These invariants are used to validate the protocol. The validation performed on the designed protocol confirms the liveness, deadlock freeness, 1-boundedness or safeness and recovery from failure properties of the protocol. For the sake of illustration, only one failure mode i.e., the corruption of messages at the receiving end is considered. However, on similar lines other modes of failure can also be considered in the design. The methodology developed in this thesis can also be used in other DCS applications such as distributed industrial control and distributed data processing.