Computer Science Department
School of Computer Science, Carnegie Mellon University
Towards a Formal Treatment of Implicit Invocation
Jurgen Dingel, David Garlan, Somesh Jha, David Notkin*
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.
*University of Washington, Seattle, Washington