Abstract

With the increasing use of software in many systems like telecommunications, e-commerce, manufacturing, etc., and the need for reliable services in these systems, there is an ever-growing demand for providing fault-tolerance. Generally, software is built without concentrating much on the fault-tolerant aspect, and fault-tolerance is typically an additional feature to ensure reliability if ever a failure has been encountered. However, there are many legacy software systems that are being deployed in highly critical applications where fault tolerance is inevitable. Various methods have been put forth in the literature for designing fault-tolerance, including a component-based methodology, wherein fault-tolerance is separated from the functionality, and fault-tolerant components, such as correctors and detectors, are added to achieve the desired reliability. Utilizing the concepts of the component-based design, we propose a category theoretic framework for the composition of these fault-tolerant components with a fault-intolerant program. We illustrate our proposed approach to compose the fault-tolerant components with a fault-intolerant program to result in a final fault-tolerant program through two case studies. In our first case study, we show the feasibility of our approach by composing the fault-tolerant components for a distributed mutual exclusion algorithm using our proposed approach. In the second case study, we decompose the fault-tolerant Label Distribution Protocol and prove the correctness of the design of the fault-tolerant components. Furthermore, the formal specification and verification of these case studies has been conducted using Specware. Some of the benefits of the proposed approach include (a) traceability of all the sorts, operations and properties used to derive the composed program, (b) well-defined interfaces, that allows components to interact in a well-specified behaviour, and (c) reuse of specification for subsequent similar system design.