Abstract

This paper presents an algorithm for deriving executable assertions that can be evaluated in a faulty distributed environment. A transformation from the global auxiliary variable approach into a new proof system based on the history of the auxiliary variables is introduced. This transformation, which matches the operational distributed environment more closely than the global auxiliary variable system, is then shown to retain the properties of this system such as noninterference, satisfaction, soundness, and completeness. An example is presented in which a model problem is transformed from one system into the other.

Department(s)

Computer Science

Comments

This work was supported in part by the National Science Foundation under Grant Numbers MIP-8909749 and CDA-8820714, and in part by the AMOCO Faculty Development Program.

Report Number

CSc-92-01

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

21 March 1992

Share

 
COinS