Verification of lack of emergent behavior in extending a social network of agents

The scalability of the system is of vital importance in the design of social networks. This research attempts to establish a comprehensive framework for analysis and validation of requirements and design documents for software systems. In previous work, we applied this framework to analyze the requirements of a social network of agents with respect to scalability of the system. In our approach, system requirements were expressed using scenario-based specifications. Scenarios are appealing because of their expressive power and simplicity. Moreover, due to the clear and concise notation of scenarios, they can be used to analyze the system requirements for general validity, lack of deadlock, and existence of emergent behavior. In this paper a methodology is presented to formally verify that certain scenarios do not emerge in the system’s behavior. This methodology is devised to indicate whether or not the new requirements of the system are consistent with the current requirements in place. A larger prototype of a social network of MSA for semantic search is utilized to illustrate the developed methodology.