Playing with time in publish-subscribe using a domain-specific model checker

ABSTRACT

Thanks to the sharp decoupling it fosters, the Publish-Subscribe paradigm is particularly suited to the implementation of dynamic applications where components join and leave the system unpredictably, and their distributed interactions change over time. Although this feature represents an asset during the implementation phases, it is usually difficult to reason on the global behavior at design time. The problem is exacerbated by the variety of Publish-Subscribe systems available that greatly differ in the guarantees provided, e.g., in terms of message reliability or delivery order.

Some of the authors already tackled the problem with a domain-specific model checker, whose internals are customized depending on the guarantees assumed on the communication infrastructure. However, we essentially disregarded the timing aspects, which are nonetheless pivotal in many applications exploiting a Publish-Subscribe infrastructure. In this paper we augment our tool to verify temporal properties, and explore the interplay between time and different Publish-Subscribe semantics through a case study. Moreover, we report on an effort to formally verify the correctness of the temporal extension, in an attempt to provide a strong foundation for the results obtained using our tool.

REFERENCES

• 1: R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. of the 5^th Int. Symposium on Logic in Computer Science, 1990.
• 2: Luciano Baresi , Carlo Ghezzi , Luca Mottola, On Accurate Automatic Verification of Publish-Subscribe Architectures, Proceedings of the 29th international conference on Software Engineering, p.199-208, May 20-26, 2007 [doi>10.1109/ICSE.2007.57]
• 3: Maurice H. ter Beek , Mieke Massink , Diego Latella , Stefania Gnesi , Alessandro Forghieri , Maurizio Sebastianis, A case study on the automated verification of groupware protocols, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062560]
• 4: Bogor Extensions for LTL Checking. projects.cis.ksu.edu/projects/gudangbogor/.
• 5: Jeremy S. Bradbury , Juergen Dingel, Evaluating and improving the automatic analysis of implicit invocation systems, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 6: Mauro Caporuscio , Paola Inverardi , Patrizio Pelliccione, Compositional Verification of Middleware-Based Software Architecture Descriptions, Proceedings of the 26th International Conference on Software Engineering, p.221-230, May 23-28, 2004
• 7: Nuno Carvalho , Filipe Araujo , Luis Rodrigues, Reducing Latency in Rendezvous-Based Publish-Subscribe Systems for Wireless Ad Hoc Networks, Proceedings of the 26th IEEE International ConferenceWorkshops on Distributed Computing Systems, p.28, July 04-07, 2006 [doi>10.1109/ICDCSW.2006.89]
• 8: Antonio Carzaniga , David S. Rosenblum , Alexander L. Wolf, Design and evaluation of a wide-area event notification service, ACM Transactions on Computer Systems (TOCS), v.19 n.3, p.332-383, Aug. 2001 [doi>10.1145/380749.380767]
• 9: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 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 1^st Int. Symposium on Formal Methods for Components and Objects, 2002.
• 11: DJProf Java Profiler, www.mcs.vuw.ac.nz/djp/djprof/.
• 12: Bryan S. Doerr , David C. Sharp, Freeing product line architectures from execution dependencies, Proceedings of the first conference on Software product lines : experience and research directions: experience and research directions, p.313-329, November 2000, Denver, Colorado, United States
• 13: Patrick Th. Eugster , Pascal A. Felber , Rachid Guerraoui , Anne-Marie Kermarrec, The many faces of publish/subscribe, ACM Computing Surveys (CSUR), v.35 n.2, p.114-131, June 2003 [doi>10.1145/857076.857078]
• 14: David Garlan , Serge Khersonsky, Model Checking Implicit-Invocation Systems, Proceedings of the 10th International Workshop on Software Specification and Design, p.23, November 05-07, 2000
• 15: G. Gerosa. Design and Implementation of a Time Extension for a Domain-Specific Model Checker. Master Thesis (in italian), Politecnico di Milano (Italy), 2007.
• 16: Timothy H. Harrison , David L. Levine , Douglas C. Schmidt, The design and performance of a real-time CORBA event service, Proceedings of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.184-200, October 05-09, 1997, Atlanta, Georgia, United States
• 17: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 18: 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), June 2004.
• 19: Robby , Matthew B. Dwyer , John Hatcliff, Bogor: an extensible and highly-modular software model checking framework, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 20: Upkar Varshney, Pervasive Healthcare, Computer, v.36 n.12, p.138-140, December 2003 [doi>10.1109/MC.2003.1250897]
• 21: L. Zanolin, C. Ghezzi, and L. Baresi. An approach to model and validate publish/subscribe architectures. In Proc. of the SAVCBS Workshop, 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Patterns (e.g., client/server, pipeline, blackboard)

General Terms:
Verification

Keywords:
distributed architectures, model checking, modeling, publish-subscribe, time