Towards a Formal Treatment of Implicit Invocation
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
Implicit invocation SN92,GN91 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 relyguarantee reasoning for concurrent systems Jon83,Stphi91. The application of the framework is illustrated with several examples. The merits and limitations of the relyguarantee paradigm in the context of implicit invocation systems are also discussed.
- Computer Systems