Abstract: Towards a Formal Treatment of Implicit Invocation using Rely/Guarantee Reasoning
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~\cite{Jon83,Sto91}.
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.
Home