Towards a formal treatment of implicit invocation.
Authors: J. Dingel, D. Garlan, S. Jha, and D. Notkin
To appear in Formal Aspects of Computing
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.