Abstract

Distributed algorithms can use executable assertions, which can be derived from program verificatioll or specified in an ad hoc manner, to detect. errors at run-time. However, there may be more assertions available than are really unecessary, and embedding all of them into the program to be checked at run-time would make error-detection very inefficient. For safety-critical systems we often need to make decisions very quickly and cannot allow too much time to be spent on error detection.

The new technique of temporal submission, which is introduced in this dissertation, examines the dependencies between the individual assertions along program execution paths. In contrast to classical subsumption, where aII logical expressions to be examined are true simultaneously, a program assertion need only be true when the corresponding statement in the distributed program has just been executed. Thus, temporal subsumption, based on the set of assertions (derived from a verification proof or ad hoc assertions) and in combination with the set of all legal states in the system, allows for the removal of redundant (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 errors caused by a faulty process based on the information it receives from the faulty process.

Temporal subsumption makes error detection more efficient than conventional methods, in addition Lo maintaining the same fault detection latency as the complete set of assertions. This is especially important for fault-tolerant responsive systems, where we want to detect errors as soon as possible with very little computational overhead.

To validate the theory, a tool was developed to perform subsumption automatically. For ad hoc assertions, this tool can be complemented with a weakest pre-condition generation system that allows the generation of additional assertions. Using these tools, it was detected how temporal subsumption can also be used as a proof checker. Such a checker allows us to determine whether a given argument of program correctness contains errors.

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 Summer 1994.

Report Number

CSc-94-18

Document Type

Technical Report

Document Version

Final Version

File Type

text

Language(s)

English

Rights

© 1994 University of Missouri - Rolla, All rights reserved

Publication Date

1 June, 1994

Download

Share

 
COinS