Manohar, Rajit and Sivilotti, Paolo A. G. (1996) Composing Processes Using Modified Rely-Guarantee Specifications. California Institute of Technology . (Unpublished) http://resolver.caltech.edu/CaltechCSTR:1996.cs-tr-96-22
See Usage Policy.
Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCSTR:1996.cs-tr-96-22
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)|
|Group:||Computer Science Technical Reports|
|Usage Policy:||You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.|
|Deposited By:||Imported from CaltechCSTR|
|Deposited On:||25 Apr 2001|
|Last Modified:||26 Dec 2012 14:05|
Repository Staff Only: item control page