Evaluating and Improving the Automatic Analysis of Implicit Invocation Systems

by Jeremy S. Bradbury, Juergen Dingel


Model checking and other finite-state analysis techniques have been very successful when used with hardware systems and less successful with software systems. It is especially difficult to analyze software systems developed with the implicit invocation architectural style because the loose coupling of their components increases the size of the finite state model. In this paper we extend an existing approach to model checking implicit invocation to allow for the modeling of larger and more realistic systems. Our focus will be on improving the representation of events, event delivery policies and event-method bindings. We also evaluate our technique on two non-trivial examples. In one of our examples, we will show how with iterative analysis a system parameter can be chosen to meet the appropriate system requirements.

Bibliographic Information [Bibtex format]

Author = {Jeremy S. Bradbury and Juergen Dingel},
Booktitle = {In Proc. of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003)},
Month = {Sept.},
Pages = {78-87},
Title = {Evaluating and Improving the Automatic Analysis of Implicit Invocation Systems},
Year = {2003}}

Paper: [PDF]   Presentation: [PDF]