Model Checking Implicit-Invocation Systems

While implicit invocation (publish-subscribe) systems have goodengineering properties, they are difficult toreason about and to test. Model checking such systems is an attractive alternative. 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. Keywords Implicit invocation, publish-subscribe, model checking.

• Type: Conference
• Year: 2000
• Where: IWSSD
• Authors: David Garlan, Serge Khersonsky
• Keywords: Implicit Invocation, Implicit Invocation System, IWSSD 2000, Model Checking, Software Engineering