Abstract

An important aspect which is often overlooked in the software design cycle is the question of assurance. Many methodologies in the past have attempted to provide assurance efficiently, but have never been sucessful at eliminating explicit time and space redundancy. One approach is the Application-Oriented Fault Tolerance Paradigm, which provides assurance by examining the behavior and propenies of the application and deriving executable assertions for the detection of faults. Previous work has demonstrated the feasibility of the application-oriented fault tolerance paradigm for various applications. However, the executable assertions were guided by the natural constraints of the problem. This work focuses on developing a formal basis for applying concurrent programming axiomatic proof systems to formally generate executable assertions in a distributed environment, which has resulted in giving the area of application-oriented fault tolerance a mathematical structure, thus allowing us to reason about application-oriented fault tolerance with known methods. The result is the development of a method of transforming a verification proof outline of a concurrent program to a fault-tolerant program by convening intermediate assenions to executable assertions.

Department(s)

Computer Science

Comments

The first Author is a Graduate Student.

This report is substantially the Ph.D. dissertation of the first author, completed July 1992.

Report Number

CSc-92-25

Document Type

Technical Report

Document Version

Final Version

File Type

text

Language(s)

English

Rights

© 1992 University of Missouri - Rolla, All rights reserved

Publication Date

1 July, 1992

Download

Share

 
COinS