Technical Report CS0388

Title: Proving Noninteraction: an Optimized Approach
Authors: R. Gerth and L. Shrira
Abstract: A recent work of Elrad and Francez introduces a novel methodology of analyzing distributed programs: decomposition into communication closed layers i.e. no interaction occurs between layers. This work proposes an optimization to the formal proof of layer non-interaction. The proof is localized to the bodies of component layers only. By this, the number of possible interaction cases to be considered in the proof is reduced substantially. Our main result contains a definition of new localized communication closeness and a suggestion of a sound and complete proof rule for proving layer non-interaction. The proof rule is maximaly efficient in the sense that it makes use only of the correctness proof of the layer itself. The obtained result, in addtion to program analysis, also sheds new light on the use of closed layer methodology in the construction of distributed programs.
CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (, rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the CS technical reports of 1985
To the main CS technical reports page

Computer science department, Technion