Published June 12, 1996
| Submitted
Technical Report
Open
Composing Processes Using Modified Rely-Guarantee Specifications
- Creators
- Manohar, Rajit
- Sivilotti, Paolo A. G.
Chicago
An error occurred while generating the citation.
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
- Eprint ID
- 26801
- Resolver ID
- CaltechCSTR:1996.cs-tr-96-22
- Air Force Office of Scientific Research (AFOSR)
- 91-0070
- NSF
- CCR-912008
- NSF
- CCR-9527130
- IBM
- Army Research Office (ARO)
- Defense Advanced Research Projects Agency (DARPA)
- Created
-
2001-04-25Created from EPrint's datestamp field
- Updated
-
2019-10-03Created from EPrint's last_modified field
- Caltech groups
- Computer Science Technical Reports