Towards a Formal Treatment of Implicit Invocation using Rely-Guarantee ReasoningJurgen Dingel, David Garlan, Somesh Jha, and David NotkinFormal Aspects of Computing, 10:193-213, 1998.
|
||||
Abstract | ||||
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. | ||||
Keywords | ||||
Implicit invocation, rely/guarantedd reasoning, assumption/commitment reasoning, formal methods, software architecture | ||||
|
Last modified: 10/15/2001. For comments and problems, contact able-help@cs.cmu.edu.