Abstract

Distributed algorithms can use executable assertions derived from program verification to detect errors at run-time. However, a complete verification proof outline contains a large number of assertions, and embedding all of them into the program to be checked at run-time would make error-detection very inefficient.

The technique of temporal subsumption examines the dependencies between the individual assertions along program execution paths. In contrast to classical subsumption, where all logical expressions to be examined are true simultaneously, an assertion need only be true when the corresponding statement in the distributed program has been executed. Thus, temporal subsumption based on the set of assertions derived from a verification proof and in combination with the set of all legal states in the system, allows for the removal of (partial) assertions along execution sequences.

We assume a fault model of Byzantine (malicious) behavior, and therefore an individual process cannot check itself for faults. We assume that a non-faulty process will always perform the correct computation so that once external data (obtained through communication) has been verified, the local computation does not need to be checked. A non-faulty process can thus detect faults produced by a faulty process based on the information it receives from it.

Department(s)

Computer Science

Comments

This work was supported in part by the National Science Foundation under Grant Numbers MSS- 9216479 and CDA-9222827, and, in part, from the Air Force Office of Scientific Research under contract numbers F49620-92-J-0546 and F49620-93-I-0409 and, in part, by a grant from the University of Missouri Research Board.

Report Number

CSC-93-28

Document Type

Technical Report

Document Version

Final Version

File Type

text

Language(s)

English

Rights

© 1993 University of Missouri--Rolla, All rights reserved.

Publication Date

21 Oct 1993

Download

Share

 
COinS