<%@ page language="java" contentType="text/html" %> <%-- Include common initialisation code --%> <%@ include file="/arch/common.jsp" %> <%-- The current tab --%> <% String currentTab = "Research"; %> <%-- Content of navigation pane --%> <%@ include file="nav.jsp" %> <% showCurrentLink=true; %> <%-- Current navigation location --%> <% String currentNav = "Reports and Theses"; %> <%-- Include the code for the document header --%> <%@ include file="/arch/header.jsp" %>

Research Report CS-RR-237

<%-- Include the code for the lines and navigation --%> <%@ include file="/arch/middle.jsp" %>

Doron Peled and M. Joseph, A Compositional Framework for Fault-Tolerance by Specification Transformation (January 1, 1993).

Abstract

The incorporation of a recovery algorithm into a program can be viewed as a program transformation, converting the basic program into a fault-tolerant version. We present a framework in which such program transformations are accompanied by a corresponding formula transformation which obtains properties of the fault-tolerant versions of the programs from properties of the basic programs. Compositionality is achieved when every property of the fault-tolerant version can be obtained from a transformed property of the basic program. A verification method for proving the correctness of formula transformations is presented. This makes it possible to prove just once that a formula transformation corresponds to a program transformation, removing the need to prove separately the correctness of each transformed program. Keywords: Parallel Algorithms, Distributed Algorithms, Fault-Tolerance, Specification, Verification.

<%@ include file="cited.html" %>

D. Peled and M. Joseph, "A Compositional Framework for Fault-tolerance by Specification Transformation", Theoretical Computer Science 128, pp. 99-125 (1994)

<%-- Include the code for the document footer --%> <%@ include file="/arch/footer.jsp" %>