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

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

Z. Liu and M. Joseph, Verification of Fault-Tolerance and Real-Time (March 1, 1996).

Abstract

A transformational method is given for specifying and verifying fault-tolerant real-time programs. Such a program needs to be provably correct according to its both functional and real-time requirements, despite the presence of possible system failures. The paper demonstrates that a suitably expressive logic for real-time systems allows to naturally model the state changes by system failures and determine their effect on the functional and real-time properties of executions.

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

Z. Liu and M. Joseph, "Verification of Fault-Tolerance and Real-Time", Proceedings of the 26th IEEE FTCS, Japan, IEEE, pp. 220-229 (1996)

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