More Web Proxy on the site http://driver.im/

Article

On Accurate Automatic Verification of Publish-Subscribe Architectures

Authors:

Luciano Baresi,

Luca MottolaAuthors Info & Claims

ICSE '07: Proceedings of the 29th international conference on Software Engineering

Pages 199 - 208

https://doi.org/10.1109/ICSE.2007.57

Published: 24 May 2007 Publication History

Abstract

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.

References

[1]

{1} M. Autili, P. Inverardi, and P. Pelliccione. A scenario based notation for specifying temporal properties. In Proc. of the 2006 Int. Wkshp. on Scenarios and state machines: models, algorithms, and tools, pages 21-28, 2006.

Digital Library

[2]

{2} L. Baresi, C. Ghezzi, and L. Mottola. Towards fine-grained automated verification of publish-subscribe architectures. In Proc. of the 26th Int. Conf. on Formal Methods for Networked and Distributed Systems (FORTE06), pages 131-135, 2006.

Digital Library

[3]

{3} M.-H. Beek, M. Massink, D. Latella, S. Gnesi, A. Forghieri, and M. Sebastianis. A case study on the automated verification of groupware protocols. In Proc. of the 27th Int. Conf. on Software engineering (ICSE05), pages 596-603, 2005.

Digital Library

[4]

{4} S. Bhola, R. E. Strom, S. Bagchi, Y. Zhao, and J. S. Auerbach. Exactly-once delivery in a content-based publish-subscribe system. In Proc. of the 2002 Int. Conf. on Dependable Systems and Networks, pages 7-16, 2002.

Digital Library

[5]

{5} Bogor Extensions for LTL Checking. projects.cis.ksu. edu/projects/gudangbogor/.

[6]

{6} J.-S. Bradbury and J. Dingel. Evaluating and improving the automatic analysis of implicit invocation systems. In Proc. of the 9th European software engineering Conf., pages 78-87, 2003.

Digital Library

[7]

{7} M. Caporuscio, P. Inverardi, and P. Pelliccione. Compositional verification of middleware-based software architecture descriptions. In Proc. of the 19th Int. Conf. on Software engineering (ICSE04), pages 221-230, 2004.

Digital Library

[8]

{8} A. Carzaniga, D.-S. Rosenblum, and A.-L. Wolf. Design and evaluation of a wide-area event notification service. ACM Trans. Comput. Syst., 19(3), 2001.

Digital Library

[9]

{9} J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, Robby, and H. Zheng. Bandera: extracting finite-state models from java source code. In Proc. of the 22nd Int. Conf. on Software engineering, pages 439-448, 2000.

Digital Library

[10]

{10} X. Deng, M.-B. Dwyer, J. Hatcliff, and G. Jung. Model-checking middleware-based event-driven real-time embedded software. In Proc. of the 1st Int. Symposium on Formal Methods for Components and Objects, pages 154-181, 2002.

[11]

{11} P.-T. Eugster, P.-A. Felber, R. Guerraoui, and A.-M. Kermarrec. The many faces of publish/subscribe. ACM Comput. Surv., 35(2), 2003.

Digital Library

[12]

{12} D. Garlan and S. Khersonsky. Model checking implicit-invocation systems. In Proc. of the 10th Int. Workshop on Software Specification and Design, 2000.

Digital Library

[13]

{13} D. Garlan, S. Khersonsky, and J. Kim. Model checking publish-subscribe systems. In Proc. of the 10th Int. SPINWorkshop on Model Checking Software (SPIN03), pages 166-180, 2002.

Digital Library

[14]

{14} J. Hatcliff, X. Deng, M.-B. Dwyer, G. Jung, and V. Ranganath. Cadena: an integrated development, analysis, and verification environment for component-based systems. In Proc. of the 25th Int. Conf. on Software Engineering (ICSE03), pages 160-173, 2003.

Digital Library

[15]

{15} G. J. Holzmann. The model checker spin. IEEE Trans. Softw. Eng., 23(5):279-295, 1997.

Digital Library

[16]

{16} IBM Research. The Gryphon Middleware. www.research.ibm. com/gryphon.

[17]

{17} S. Li, Y. Lin, S. H. Son, J. A. Stankovic, and Y. Wei. Event detection services using data service middleware in distributed sensor networks. Telecommunication Systems, 26(2):351-368, June 2004.

Digital Library

[18]

{18} S. Madden, M. J. Franklin, J. M. Hellerstein, and W. Hong. TinyDB: an acquisitional query processing system for sensor networks. ACM Trans. Database Syst., 30(1):122-173, 2005.

Digital Library

[19]

{19} L. Mottola. Accurate Verification of Publish-Subscribe Architectures. Technical report, Politecnico di Milano, Italy, 2006.

[20]

{20} Robby, M.-B. Dwyer, and J. Hatcliff. Bogor: an extensible and highly-modular software model checking framework. In Proc. of the 9th European software engineering Conf., pages 267-276, 2003.

Digital Library

[21]

{21} Sun Microsystems. JMS Specifications and Reference Implementation. java.sun.com/products/jms/docs.html.

[22]

{22} A. Woo, T. Tong, and D. Culler. Taming the underlying challenges of reliable multihop routing in sensor networks. In Proc. of the 1st Int. Conf. on Embedded networked sensor systems (SENSYS03), pages 14-27, 2003.

Digital Library

[23]

{23} L. Zanolin, C. Ghezzi, and L. Baresi. An approach to model and validate publish/subscribe architectures. In Proc. of the SAVCBS'03 Workshop, pages 35-41, 2003.

[24]

{24} H. Zhang, J. S. Bradbury, J. R. Cordy, and J. Dingel. Implementation and verification of implicit-invocation systems using source transformation. In Proc. of the 5th Int. Wkshp. on Source Code Analysis and Manipulation (SCAM05), pages 87-96, 2005.

Digital Library

Cited By

Toman SLahouij AKotel SHamel LToman ZGraiet M(2024)Service to service communication based on CBPS system: refinement and verificationSoft Computing - A Fusion of Foundations, Methodologies and Applications10.1007/s00500-024-09902-w28:19(10943-10963)Online publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1007/s00500-024-09902-w
Paraponiari PRahonis G(2022)Weighted propositional configuration logicsInformation and Computation10.1016/j.ic.2020.104647282:COnline publication date: 1-Jan-2022
https://dl.acm.org/doi/10.1016/j.ic.2020.104647
Suresh VChakrabarti SJetley RNaik RSarkar SHildebrandt TKumar ASharma R(2019)Automated Test Case Generation for Programmable Logic Controller CodeProceedings of the 12th Innovations in Software Engineering Conference (formerly known as India Software Engineering Conference)10.1145/3299771.3299799(1-4)Online publication date: 14-Feb-2019
https://dl.acm.org/doi/10.1145/3299771.3299799
Show More Cited By

Index Terms

On Accurate Automatic Verification of Publish-Subscribe Architectures

Recommendations

Towards fine-grained automated verification of publish-subscribe architectures
FORTE'06: Proceedings of the 26th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems

The design and validation of distributed applications built on top of Publish-Subscribe infrastructures remain an open problem. Previous efforts adopted finite automata to specify the components’ behavior, and model checking to verify global properties. ...
Model-checking verification of publish-subscribe architectures in web service contexts
SAC '15: Proceedings of the 30th Annual ACM Symposium on Applied Computing

In this paper we consider a Timed Automata model for the Publish/Subscribe paradigm, where special attention is given to its temporal aspects. Despite this special interest, we present a generic model for publishing and managing WS-resourses in the ...
Automatic verification of parameterized systems

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '07: Proceedings of the 29th international conference on Software Engineering

May 2007

784 pages

ISBN:0769528287

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

IEEE Computer Society

United States

Publication History

Published: 24 May 2007

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
428
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 31 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Toman SLahouij AKotel SHamel LToman ZGraiet M(2024)Service to service communication based on CBPS system: refinement and verificationSoft Computing - A Fusion of Foundations, Methodologies and Applications10.1007/s00500-024-09902-w28:19(10943-10963)Online publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1007/s00500-024-09902-w
Paraponiari PRahonis G(2022)Weighted propositional configuration logicsInformation and Computation10.1016/j.ic.2020.104647282:COnline publication date: 1-Jan-2022
https://dl.acm.org/doi/10.1016/j.ic.2020.104647
Suresh VChakrabarti SJetley RNaik RSarkar SHildebrandt TKumar ASharma R(2019)Automated Test Case Generation for Programmable Logic Controller CodeProceedings of the 12th Innovations in Software Engineering Conference (formerly known as India Software Engineering Conference)10.1145/3299771.3299799(1-4)Online publication date: 14-Feb-2019
https://dl.acm.org/doi/10.1145/3299771.3299799
Liu YGuan YLi XWang RZhang JHu KZhan N(2018)Formal analysis and verification of DDS in ROS2Proceedings of the 16th ACM-IEEE International Conference on Formal Methods and Models for System Design10.5555/3343872.3343880(62-66)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.5555/3343872.3343880
Guo SWu MWang CBodden ESchäfer WDeursen AZisman A(2017)Symbolic execution of programmable logic controller codeProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106245(326-336)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106245
Bouloukakis GGeorgantas NKattepur AIssarny VBinder WCortellessa VKoziolek ASmirni EPoess M(2017)Timeliness Evaluation of Intermittent Mobile Connectivity over Pub/Sub SystemsProceedings of the 8th ACM/SPEC on International Conference on Performance Engineering10.1145/3030207.3030220(275-286)Online publication date: 17-Apr-2017
https://dl.acm.org/doi/10.1145/3030207.3030220
Garcia JPopescu DSafi GHalfond WMedvidovic NMeyer BBaresi LMezini M(2013)Identifying message flow in distributed event-based systemsProceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering10.1145/2491411.2491462(367-377)Online publication date: 18-Aug-2013
https://dl.acm.org/doi/10.1145/2491411.2491462
Lucas CElbaum SRosenblum D(2012)Detecting problematic message sequences and frequencies in distributed systemsACM SIGPLAN Notices10.1145/2398857.238468347:10(915-926)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2398857.2384683
Lucas CElbaum SRosenblum DLeavens GDwyer M(2012)Detecting problematic message sequences and frequencies in distributed systemsProceedings of the ACM international conference on Object oriented programming systems languages and applications10.1145/2384616.2384683(915-926)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384616.2384683
Bagherzadeh MRajan HLeavens GMooney SBorba PChiba S(2011)Translucid contractsProceedings of the tenth international conference on Aspect-oriented software development10.1145/1960275.1960293(141-152)Online publication date: 21-Mar-2011
https://dl.acm.org/doi/10.1145/1960275.1960293
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents