Towards a formal treatment of implicit invocation using rely/guarantee reasoning
Jurgen Dingel,
David Garlan, Somesh Jha and David Notkin.
In Formal Aspects of Computing, Vol. 1-:193-213, 1998. Supersedes CMU-CS-97-153.
Online links:    Plain Text
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, Formal Methods, Software Architecture.
|
|
