Checking the robustness of a Message Oriented Middleware based system

The publish/subscribe paradigm is used to support a many-to-many model that allows an efficient dissemination of messages across a distributed system. Message Oriented Middleware (MOM) is a middleware that provides an asynchronous method of passing information between networked applications. MOMs can be based on a publish/subscribe model, which offers a robust paradigm for message delivery. This paper is concerned with this specific type of MOM. Recently, systems using MOMs have been used to integrate enterprise systems over geographically distributed areas, like the ones used in financial services, telecommunication applications, transportation and health-care systems. However, the reliability of a MOM system must be verified as well as the guarantees of delivery and reachability to all intended destinations. This paper provides a suitable way of checking the configuration of a publish/subscribe MOM system by building a model and using Linear-time Temporal Logic and Computation Tree Logic rules to verify certain constraints. In addition a code generator and a sub-paths detector are implemented to make the system checking more user-friendly and efficient.