This Article 
 Bibliographic References 
 Add to: 
Loupe: Verifying Publish-Subscribe Architectures with a Magnifying Lens
March/April 2011 (vol. 37 no. 2)
pp. 228-246
Luciano Baresi, Politecnico di Milano, Milano
Carlo Ghezzi, Politecnico di Milano, Milano
Luca Mottola, Politecnico di Milano, Milano
The Publish-Subscribe (P/S) communication paradigm fosters high decoupling among distributed components. This facilitates the design of dynamic applications, but also impacts negatively on their verification, making it difficult to reason on the overall federation of components. In addition, existing P/S infrastructures offer radically different features to the applications, e.g., in terms of message reliability. This further complicates the verification as its outcome depends on the specific guarantees provided by the underlying P/S system. Although model checking has been proposed as a tool for the verification of P/S architectures, existing solutions overlook many characteristics of the underlying communication infrastructure to avoid state explosion problems. To overcome these limitations, the Loupe domain-specific model checker adopts a different approach. The P/S infrastructure is not modeled on top of a general-purpose model checker. Instead, it is embedded within the checking engine, and the traditional P/S operations become part of the modeling language. In this paper, we describe Loupe's design and the dedicated state abstractions that enable accurate verification without incurring state explosion problems. We also illustrate our use of state-of-the-art software verification tools to assess some key functionality in Loupe's current implementation. A complete case study shows how Loupe eases the verification of P/S architectures. Finally, we quantitatively compare Loupe's performance against alternative approaches. The results indicate that Loupe is effective and efficient in enabling accurate verification of P/S architectures.

[1] ActiveMQ, Home Page,, 2010.
[2] R. Alur, C. Courcoubetis, and D. Dill, “Model Checking for Real-Time Systems,” Proc. Fifth Int'l Symp. Logic in Computer Science, 1990.
[3] L. Baresi, G. Gerosa, C. Ghezzi, and L. Mottola, “Playing with Time in Publish-Subscribe Using a Domain-Specific Model Checker,” Proc. Specification and Verification of Component-Based Systems Workshop, 2007.
[4] L. Baresi, C. Ghezzi, and L. Mottola, “Towards Fine-Grained Automated Verification of Publish-Subscribe Architectures,” Proc. 26th Int'l Conf. Formal Methods for Networked and Distributed Systems, 2006.
[5] L. Baresi, C. Ghezzi, and L. Mottola, “On Accurate Automatic Verification of Publish-Subscribe Architectures,” Proc. 29th Int'l Conf. Software Eng., 2007.
[6] L. Baresi, C. Ghezzi, and L. Mottola, “Accurate Verification of Publish-Subscribe Architectures,” technical report, Politecnico di Milano, 2008.
[7] M.-H. Beek, M. Massink, D. Latella, S. Gnesi, A. Forghieri, and M. Sebastianis, “Model Checking Publish-Subscribe Notification for Thinkteam,” Proc. Ninth Int'l Workshop Formal Methods for Industrial Critical Systems, 2004.
[8] M.-H. Beek, M. Massink, D. Latella, S. Gnesi, A. Forghieri, and M. Sebastianis, “A Case Study on the Automated Verification of Groupware Protocols,” Proc. 27th Int'l Conf. Software Eng., 2005.
[9] S. Bhola, R.E. Strom, S. Bagchi, Y. Zhao, and J.S. Auerbach, “Exactly-Once Delivery in a Content-Based Publish-Subscribe System,” Proc. Int'l Conf. Dependable Systems and Networks, 2002.
[10] Bogor Project, Extensions for LTL Checking, , 2010.
[11] J.-S. Bradbury and J. Dingel, “Evaluating and Improving the Automatic Analysis of Implicit Invocation Systems,” Proc. Ninth European Software Eng. Conf., 2003.
[12] M. Caporuscio, P. Inverardi, and P. Pelliccione, “Compositional Verification of Middleware-Based Software Architecture Descriptions,” Proc. 19th Int'l Conf. Software Eng., 2004.
[13] A. Carzaniga, D.-S. Rosenblum, and A.-L. Wolf, “Design and Evaluation of a Wide-Area Event Notification Service,” ACM Trans. Computer Systems, vol. 19, no. 3, pp. 332-383, 2001.
[14] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 1999.
[15] D. Colangelo, D. Compare, P. Inverardi, and P. Pelliccione, “Reducing Software Architecture Models Complexity: A Slicing and Abstraction Approach,” Proc. 26th Int'l Conf. Formal Methods for Networked and Distributed Systems, 2006.
[16] K. Compton, Y. Gurevich, J. Huggins, and W. Shen, “An Automatic Verification Tool for UML,” Technical Report CSE-TR-423-00, Univ. of Michigan, 2000.
[17] J.C. Corbett, M.B. Dwyer, J. Hatcliff, S. Laubach, C.S.P. Robby, and H. Zheng, “Bandera: Extracting Finite-State Models from Java Source Code,” Proc. 22nd Int'l Conf. Software Eng., 2000.
[18] J.C. Corbett, M.B. Dwyer, J. Hatcliff, and Robby, “A Language Framework for Expressing Checkable Properties of Dynamic Software,” Proc. Seventh SPIN Workshop, 2000.
[19] P. Costa, G. Coulson, R. Gold, M. Lad, C. Mascolo, L. Mottola, G.P. Picco, T. Sivaharan, N. Weerasinghe, and S. Zachariadis, “The RUNES Middleware for Networked Embedded Systems and Its Application in a Disaster Management Scenario,” Proc. Fifth Int'l Conf. Pervasive Comm., 2007.
[20] P. Costa, M. Migliavacca, G.P. Picco, and G. Cugola, “Epidemic Algorithms for Reliable Content-Based Publish-Subscribe: An Evaluation,” Proc. 24th Int'l Conf. Distributed Computing Systems, 2003.
[21] G. Cugola, M. Migliavacca, and A. Monguzzi, “On Adding Replies to Publish-Subscribe,” Proc. First Int'l Conf. Distributed Event-Based Systems, 2007.
[22] G. Cugola and G.P. Picco, “REDS: A Reconfigurable Dispatching System,” Proc. Sixth Int'l Workshop Software Eng. and Middleware, 2006.
[23] D. Dailey, M. Haselkorn, and D. Meyers, “A Structured Approach to Developing Real-Time Distributed Network Applications for ITS Deployment,” The ITS J., vol. 3, no. 1, pp. 163-180, 1997.
[24] X. Deng, M.-B. Dwyer, J. Hatcliff, and G. Jung, “Model Checking Middleware-Based Event-Driven Real-Time Embedded Software,” Proc. First Int'l Symp. Formal Methods for Components and Objects, 2002.
[25] DJProf, Java Memory Profiler,, 2010.
[26] B.S. Doerr and D.C. Sharp, “Freeing Product Line Architectures from Execution Dependencies,” Proc. First Conf. Software Product Lines, 2000.
[27] P.-T. Eugster, P.-A. Felber, R. Guerraoui, and A.-M. Kermarrec, “The Many Faces of Publish/Subscribe,” ACM Computing Surveys, vol. 35, no. 2, pp. 114-131, 2003.
[28] D. Garlan and S. Khersonsky, “Model Checking Implicit-Invocation Systems,” Proc. 10th Int'l Workshop Software Specification and Design, 2000.
[29] D. Garlan, S. Khersonsky, and J. Kim, “Model Checking Publish-Subscribe Systems,” Proc. 10th Int'l SPIN Workshop, 2002.
[30] D. Gelernter, “Generative Communication in Linda,” ACM Computing Surveys, vol. 7, no. 1, pp. 80-112, 1985.
[31] S. Gnesi, D. Latella, and M. Massink, “Model Checking UML Statecharts Diagrams Using JACK,” Proc. Fourth Int'l Symp. High Assurance Systems Eng., 1999.
[32] T.H. Harrison, D.L. Levine, and D.C. Schmidt, “The Design and Performance of a Real-Time Corba Event Service,” Proc. 12th Conf. Object-Oriented Programming, Systems, Languages, and Applications, 1997.
[33] J. Hatcliff, X. Deng, M.-B. Dwyer, G. Jung, and V. Ranganath, “Cadena: An Integrated Development, Analysis, and Verification Environment for Component-Based Systems,” Proc. 25th Int'l Conf. Software Eng., 2003.
[34] F. He, L. Baresi, C. Ghezzi, and P. Spoletini, “Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata,” Proc. 27th Int'l Conf. Formal Methods for Networked and Distributed Systems, 2007.
[35] D. Heimbigner, “Adapting Publish/Subscribe Middleware to Achieve Gnutella-Like Functionality,” Proc. Eighth ACM Symp. Applied Computing, 2001.
[36] G.J. Holzmann, “The Model Checker Spin,” IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279-295, May 1997.
[37] G.J. Holzmann and R. Joshi, “Model-Driven Software Verification,” Proc. 11th Int'l SPIN Workshop, 2004.
[38] IBM Research, The Gryphon Middleware, comgryphon, 2010.
[39] P. Inverardi, H. Muccini, and P. Pelliccione, “Charmy: An Extensible Tool for Architectural Analysis,” Proc. 10th European Software Eng. Conf., pp. 111-114, 2005.
[40] S. Kalasapur, K. Senthivel, and M. Kumar, “Service Oriented Pervasive Computing for Emergency Response Systems,” Proc. Fourth IEEE Workshop Ubiquitous and Pervasive Health Care, 2006.
[41] N. Kaveh and W. Emmerich, “Deadlock Detection in Distributed Object Systems,” Proc. Eighth European Software Eng. Conf., 2001.
[42] T. Kim, Y.-T. Song, L. Chung, and D.T. Huynh, “Software Architecture Analysis: A Dynamic Slicing Approach,” ACIS Int'l J. Computer and Information Science, vol. 1, no. 2, pp. 91-103, 2000.
[43] A.D. Kshemkalyani, “The Power of Logical Clock Abstractions,” Distributed Computing, vol. 17, no. 2, pp. 131-150, 2004.
[44] A.D. Kshemkalyani and M. Singhal, Distributed Computing: Principles, Algorithms, and Systems. Cambridge Univ. Press, 2008.
[45] L. Lamport, “Time, Clocks, and the Ordering of Events in a Distributed System,” Comm. ACM, vol. 21, no. 7, pp. 558-565, 1978.
[46] S. Li, Y. Lin, S.H. Son, J.A. Stankovic, and Y. Wei, “Event Detection Services Using Data Service Middleware in Distributed Sensor Networks,” Telecomm. Systems, vol. 26, no. 2, pp. 351-368, 2004.
[47] J. Lilius and I.P. Paltor, “vUML: A Tool for Verifying UML Models,” Proc. 14th Int'l Conf. Automated Software Eng., 1999.
[48] H. Liu and H.-A. Jacobsen, “A-TOPSS: A Publish/Subscribe System Supporting Approximate Matching,” Proc. 28th Int'l Conf. Very Large Data Bases, 2002.
[49] Loupe, Home Page,, 2010.
[50] P. Merino and J.M. Troya, “Modelling and Verification of the Itu-t Multipoint Communication Service with Spin,” Proc. Second Int'l Workshop SPIN Verification, 1996.
[51] G. Muhl, L. Fiege, and P. Pietzuch, Distributed Event-Based Systems. Springer, 2006.
[52] OpenJMS, Home Page,, 2010.
[53] A. Ouksel, O. Jurca, I. Podnar, and K. Aberer, “Efficient Probabilistic Subsumption Checking for Content-Based Publish-Subscribe Systems,” Proc. Seventh ACM/USENIX Int'l Middleware Conf., 2006.
[54] Robby, M.-B. Dwyer, and J. Hatcliff, “Bogor: An Extensible and Highly-Modular Software Model Checking Framework,” Proc. Ninth European Software Eng. Conf., 2003.
[55] T. Schäfer, A. Knapp, and S. Merz, “Model Checking UML State Machines and Collaborations,” Electronic Notes in Theoretical Computer Science, vol. 55, no. 3, pp. 357-369, 2001.
[56] J. Schiefer, S. Rozsnyai, C. Rauscher, and G. Saurer, “Event-Driven Rules for Sensing and Responding to Business Situations,” Proc. First Int'l Conf. Distributed Event-Based Systems, 2007.
[57] E. Souto, G. Guimares, G. Vasconcelos, M. Vieira, N. Rosa, and C. Ferraz, “A Message-Oriented Middleware for Sensor Networks,” Proc. Second Workshop Middleware for Pervasive and Ad-Hoc Computing, 2004.
[58] Sputnic Project, Strategies for Public Transport in Cities,, 2010.
[59] Sun Microsystems, JMS Specifications and Reference Implementation,, 2010.
[60] A. Tanenbaum and M. van Steen, Distributed Systems: Principles and Paradigms. Prentice Hall, 2006.
[61] TIBCO, TIBCO Rendezvous Home Page, software/messaging/rendezvous default.jsp, 2010.
[62] L. Zanolin, C. Ghezzi, and L. Baresi, “An Approach to Model and Validate Publish/Subscribe Architectures,” Proc. Int'l Workshop Specification and Validation of Component-Based Systems, 2003.
[63] H. Zhang, J.S. Bradbury, J.R. Cordy, and J. Dingel, “A Transformational Framework for Testing and Model Checking Implicit Invocation Systems,” Proc. Int'l Workshop Distributed Event-Based Systems, 2004.
[64] H. Zhang, J.S. Bradbury, J.R. Cordy, and J. Dingel, “Implementation and Verification of Implicit-Invocation Systems Using Source Transformation,” Proc. Fifth Int'l Workshop Source Code Analysis and Manipulation, 2005.

Index Terms:
Publish-subscribe, verification, model-checking.
Luciano Baresi, Carlo Ghezzi, Luca Mottola, "Loupe: Verifying Publish-Subscribe Architectures with a Magnifying Lens," IEEE Transactions on Software Engineering, vol. 37, no. 2, pp. 228-246, March-April 2011, doi:10.1109/TSE.2010.39
Usage of this product signifies your acceptance of the Terms of Use.