Loupe:
 Verifying Publish-Subscribe Architectures with a Magnifying Lens
 

 Overview
 Documentation
 Download
  


Developers are increasingly exploiting the Publish-Subscribe (P/S) paradigm to implement sophisticated distributed applications. Although the loosely coupled interactions fostered by P/S are an asset during the design and implementation phases, developers struggle in verifying the system behavior.

To tackle this problem, we developed Loupe: a domain-specific model checker based on Bogor. In Loupe, the P/S paradigm is embedded within the checking engine, and the traditional P/S operations become first-class citizens in the modeling language. This makes it easier to model applications built on top of a P/S system. In addition, a dedicated state abstraction mechanism enables modeling P/S architectures at unprecedented levels of detail, without incurring in severe state explosion problems.


[© 2008-2010 Luca Mottola]