<%@ 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-206

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

Zhiming Liu and M. Joseph, A Transformational Approach to Specifying Recovery in Asynchronous Communicating Systems (February 1, 1992).

Abstract

This paper describes how the transformational framework developed in [Liu91, LJ92] is applied to backward error-recovery in asynchronous communicating systems. A physical fault is modelled as an atomic action which performs state transformations in the same way as any other program action. The possible effects of a set of faults on the execution of a program are described by a transformation of the program into its fault-affected version. Fault-tolerance is provided by using transformations to add recovery actions to a non-fault-tolerant program, so that the fault-affected version of the transformed program will then satisfy a required specification. Refinement transformations can be used in the development of a fault-tolerant program. This paper provides a feasible and formal way to consider existing backward recovery techniques in terms of simple transformations. Keywords: transformations, faults, checkpoints, recovery propagation.

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

Zhiming Liu and M. Joseph, "Specification and Verification of Recovery in Communicating Systems", Formal Techniques in Real-Time and Fault-Tolerant Systems, ed. J. Vytopil, Kluwer Academic, pp. 137-166 (1993)

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