Model checking implicit-invocation systems

Abstract

While implicit invocation (publish-subscribe) systems have good engineering properties, they are difficult to reason about and to test. Model checking such systems is an attractive al-ternative. However, it is not clear what kinds of state models are best suited for this. In this paper we propose a structural approach, which factors the model checking problem into two parts: behavior specific to a particular implicit invocation system, and reusable run-time infrastructure that handles event-based communication and delivery policies. The reusable portion is itself structured so that alternative run-time mechanisms may be experimented with.