Implementation Of A Formal Method For Modeling And Verifying Social Networks

Nowadays,social networks provide us with a convenient,low-cost way of communication and have become an indispensable part of people's lives.Problems in social networks are privacy leakage,structure deficiencies,and security issues,etc.These problems can be solved by formal verification of social networks,which can be used to complete the structure and privacy policies of social networks,and improve the security of social networks.So the research is become popular.Formal methods can use rigorous mathematical logic to verify whether hardware,software and system design are consistent with all or part of their specifications.Common formal methods include theorem proving,model checking and so on,they have been applied in modeling and verifying social networks.In most formal methods,social networks are manually modeled by analyzing the common characteristics of several typical social networks without automation tools.Specific properties are verified and they lack analysis and classification in general.These methods are mainly focus on a single social network,and do not study multiple social networks much.Against the situation mentioned above,a method based on Modeling,Simulation and Verification Language(MSVL)for formal modeling and verifying social networks is proposed,which is driven by properties and a modeling tool SNS2 MSVL.Firstly,properties in social networks are classified as privacy policies,user behaviors and social attributes.Then,representative properties are selected and described with Propositional Projection Temporal Logic(PPTL)formulas.Next,the data related to properties is acquired through web crawlers and stored in XML format.In addition,the SNS2 MSVL is used to translate the XML file into an MSVL program.Finally,the program with formulas is executed in an MSVL complier called MC to verify whether the properties are satisfied or not.Cases of Sina Weibo and QQ Space are illustrated to respectively show how this method works in single social network and multiple social networks.Moreover,the comparison of other formalization tools shows that our method has advantages of efficiency and robustness,and can also support large-scale programs.