Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published April 25, 2001 | Submitted
Report Open

Composing Processes Using Modified Rely-Guarantee Specifications

Abstract

We present a specification notation for components of concurrent systems and an accompanying proof methodology for reasong about the composition of these components. The specification construct is motivated by rely-guarantee pairs and by any-component program properties. The proof technique is based on an implication ladder and on two basic properties from which more complex properties are derived. Two examples illustrate the simplicity and compositionality of the model, and demonstrate how the model can be used to create structured and reusable proofs of distributed systems.

Additional Information

© 1996 California Institute of Technology June 12, 1996 This research is supported in part by AFOSR grant 91-0070, in part by NSF grants CCR 912008 and CCR 9527130, in part by an IBM Computer Science Fellowship and in part by the Defense and Advanced Research Projects Agency under the Office of Army Research.

Attached Files

Submitted - CSTR1996.pdf

Submitted - postscript.ps

Files

CSTR1996.pdf
Files (497.6 kB)
Name Size Download all
md5:5d2d763d6f69f3303910236aa8345d0a
232.6 kB Preview Download
md5:4bd051a034c16496bf01462b4a8ade5d
265.0 kB Download

Additional details

Created:
August 19, 2023
Modified:
October 24, 2023