Sciweavers

Share
ICSE
2007
IEEE-ACM

On Accurate Automatic Verification of Publish-Subscribe Architectures

9 years 5 months ago
On Accurate Automatic Verification of Publish-Subscribe Architectures
The paper presents a novel approach based on Bogor for the accurate verification of applications based on PublishSubscribe infrastructures. Previous efforts adopted standard model checking techniques to verify the application behavior, but they introduce strong simplifications on the underlying infrastructure to cope with the state space explosion problem and make automatic verification feasible. Instead of building on top of existing model checkers, our proposal embeds the asynchronous communication mechanisms of Publish-Subscribe infrastructures within Bogor. This way, Publish-Subscribe primitives become part of the specification language as additional, domain-specific, constructs. Accurate models become feasible without incurring in state space explosion problems, thus enabling the automated verification of applications on top of realistic communication infrastructures.
Luciano Baresi, Carlo Ghezzi, Luca Mottola
Added 09 Dec 2009
Updated 09 Dec 2009
Type Conference
Year 2007
Where ICSE
Authors Luciano Baresi, Carlo Ghezzi, Luca Mottola
Comments (0)
books