CaltechAUTHORS
  A Caltech Library Service

Composing Processes Using Modified Rely-Guarantee Specifications

Manohar, Rajit and Sivilotti, Paolo A. G. (1996) Composing Processes Using Modified Rely-Guarantee Specifications. California Institute of Technology , Pasadena, CA. (Unpublished) http://resolver.caltech.edu/CaltechCSTR:1996.cs-tr-96-22

[img]
Preview
Postscript - Submitted Version
See Usage Policy.

258Kb
[img] PDF - Submitted Version
See Usage Policy.

227Kb

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCSTR:1996.cs-tr-96-22

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.


Item Type:Report or Paper (Technical Report)
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.
Group:Computer Science Technical Reports
Funders:
Funding AgencyGrant Number
Air Force Office of Scientific Research (AFOSR)91-0070
NSFCCR-912008
NSFCCR-9527130
IBMUNSPECIFIED
Army Research Office (ARO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
Subject Keywords:Specifications, Composition, Distributed Systems, Rely-Guarantee
DOI:10.7907/Z9P848X3
Record Number:CaltechCSTR:1996.cs-tr-96-22
Persistent URL:http://resolver.caltech.edu/CaltechCSTR:1996.cs-tr-96-22
Usage Policy:You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.
ID Code:26801
Collection:CaltechCSTR
Deposited By: Imported from CaltechCSTR
Deposited On:25 Apr 2001
Last Modified:03 Apr 2017 16:47

Repository Staff Only: item control page