Playing with time in publish-subscribe using a domain-specific model checker
Luciano Baresi, Giorgio Gerosa, Carlo Ghezzi, Luca Mottola · 2007
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 domainspecific 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.