Towards a formal treatment of implicit invocation.

Authors: J. Dingel, D. Garlan, S. Jha, and D. Notkin

To appear in Formal Aspects of Computing

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: Software Architecture, Event Systems, Implicit Invocation

For further information, please visit the home pages of the ABLE research project and Carnegie Mellon University's Composable Systems Group.