Software Analysis of Internet Bots Using a Model Checker

Internet bots are software agents which perform automated tasks. Recently, Twitter bots have become popular and are widely used. However, in order to reduce the load on the Twitter server, one can only make a limited number of connections to the server. You therefore have to design a Twitter bot considering the total number of connections. Model Checking is a technique for verifying automatically whether a model satisfies a given specification. A number of model checkers have been developed, such as SPIN and UPPAAL. In this paper, we study how to apply model checking to analysis of load provided by a bot on the Twitter server. We give a model of a Twitter bot for the UPPAAL model checker. The bot is actually implemented on the Google App Engine. We analyze the dynamic features of the model with respect to restriction of communication with the Twitter server, using the UPPAAL model checker. Finally, we discuss the future direction of our work.