CMU-CS-97-153
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-97-153

Towards a Formal Treatment of Implicit Invocation

Jurgen Dingel, David Garlan, Somesh Jha, David Notkin*

July 1997

CMU-CS-97-153.ps


Keywords: Implicit invocation, rely-guarantee, assumption-commitment


Implicit invocation has become an important architectural style for large-scale system design and evolution. This paper addresses the lack of specification and verification formalisms for such systems. A formal computational model for implicit invocation is presented. We develop a verification framework for implicit invocation that is based on Jones' rely/guarantee reasoning for concurrent systems. The application of the framework is illustrated with several examples. The merits and limitations of the rely/guarantee paradigm in the context of implicit invocation systems are also discussed.

22 pages

*University of Washington, Seattle, Washington


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu