Model checking of the reliability of publish/subscribe structure based system

Recent studies show that Information Centric is one of the best ways to help Internet users find useful messages among a myriad of information. With the help of a publisher/subscriber structure, users could use this Information Centric System to subscribe to messages they have interest or from the ones their friends have recommended. However, with the increasing usage of smart phones and computers, one user could need several IP addresses and the scale of the network could increase dramatically. How to guarantee that a publisher/subscriber structure based system continues to work well becomes an important problem. This paper provides a suitable way of checking the configuration of a publisher/subscriber system network by using Linear-time Temporal Logic (LTL) and Computation Tree Logic (CTL). In order to apply this kind of model checking methods to a large network, a necessary model checking code generator is provided in this paper.