|
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] |
|
|