On Accurate Automatic Verification of Publish-Subscribe Architectures

Minneapolis, Minnesota May 20-May 26

DOI Bookmark:

http://doi.ieeecomputersociety.org/10.1109/ICSE.2007.57

29th International Conference on Soft ...

	This Article
	PURCHASE ARTICLE: $19 PDF HTML IEEE Xplore Subscribers
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Luciano Baresi Articles by Carlo Ghezzi Articles by Luca Mottola

	ASCII Text	x
	Luciano Baresi, Carlo Ghezzi, Luca Mottola, "On Accurate Automatic Verification of Publish-Subscribe Architectures," Software Engineering, International Conference on, pp. 199-208, 29th International Conference on Software Engineering (ICSE'07), 2007.

	BibTex	x
	@article{ 10.1109/ICSE.2007.57, author = {Luciano Baresi and Carlo Ghezzi and Luca Mottola}, title = {On Accurate Automatic Verification of Publish-Subscribe Architectures}, journal ={Software Engineering, International Conference on}, volume = {0}, year = {2007}, issn = {0270-5257}, pages = {199-208}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICSE.2007.57}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Software Engineering, International Conference on TI - On Accurate Automatic Verification of Publish-Subscribe Architectures SN - 0270-5257 SP199 EP208 A1 - Luciano Baresi, A1 - Carlo Ghezzi, A1 - Luca Mottola, PY - 2007 KW - null VL - 0 JA - Software Engineering, International Conference on ER -

Luciano Baresi, Politecnico di Milano, Italy

Carlo Ghezzi, Politecnico di Milano, Italy

Luca Mottola, Politecnico di Milano, Italy

The paper presents a novel approach based on Bogor for the accurate verification of applications based on Publish- Subscribe 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.

Citation:

Luciano Baresi, Carlo Ghezzi, Luca Mottola, "On Accurate Automatic Verification of Publish-Subscribe Architectures," icse, pp.199-208, 29th International Conference on Software Engineering (ICSE'07), 2007

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.