Hanumantharaya, Sinha, and Agarwal present a novel way of creating fault tolerant programs from fault intolerant programs, using what they call detectors and correctors. The specific domain of their application is multimedia protocols.

The authors use a case study to show how this task is accomplished. The novel part of this explanation is the way that the authors, using category theory and correctness by construction, prove the correctness of their approach.

They use the Specware software to go from algebraic language to executable code, and their technique is flawlessly demonstrated. A fault tolerant component-based multimedia protocol is presented in detail. This multimedia protocol is a label distribution protocol, very much like the multi-protocol label switching protocol, and it is depicted to be fault intolerant. The authors write the specifications of a fault-tolerant version of the protocol in algebraic language (MetaSlang), and use Specware to develop the protocol, and essentially create executable code.

To me, the main contribution of this paper is its demonstration of making a piece of software and/or protocol reliable and fail proof, even if on paper. Being able to do that in the real world has not been practical, mostly due to the lack of time and skills required to prove the correctness of a program or project. This paper makes strides to automate some of the mathematically intensive aspects of this process, and shows how the authors were able to accomplish such a task using software that is widely available.