Improved reliability of large scale publish/subscribe based MOMs using model checking

Abstract

Many software systems operate across different geographically distributed hardware platforms, operating systems and programming languages. Publish/subscribe based Message Oriented Middleware (MOM) provides loose coupling and an efficient, asynchronous and scalable way of communication. However, as the complexity of such systems increase, manual verification of reconfiguration policies becomes unrealistic. The task calls for automated means of proof-checking configuration information in order to improve the reliability of large-scale MOM systems. This paper proposes a new model checking approach with temporal logic specifications to design and verify a system configuration. Model checking is a powerful technique, however the creation of appropriate finite state models for the systems being checked are complex and difficult to use in practice by non-formalists. The research presented in this paper finds suitable abstractions that reduce the system to a finite state model. The tools we developed for the generation of such models can be easily used by non-formalists. The systems models created using our techniques manages state explosion thanks to the choices of our abstractions. An example of the use of our tools and techniques is presented for a 50 node MOM, where the reachability of all topics and the presence of loops are proof-checked.