Research And Implementation Of Runtime Verification Of WeChat Group

With the development of the Internet and mobile terminals,new social media based on the Internet continue to appear,and people's social activities increasingly rely on social applications.WeChat is an application released by Tencent in 2011.By the third quarter of 2019,the number of WeChat's monthly active accounts has reached 1.151 billion,and the number of mini-program's daily active accounts has exceeded 300 million.WeChat has the characteristics of low threshold,high real-time nature,and strong interaction and so on.People of different classes and age groups can publish their opinions on the Internet,and quickly spread information through interaction with their friends.However,some users will publish some bad information in WeChat,which will affect the harmony of the network environment.In order to pay more attention to the development of social network public opinion and guide network public sentiment,it is necessary to understand the characteristics and nature of WeChat in information spreading.When we study the WeChat system from the perspective of software,we can use software verification to determine whether its special property is satisfied.Compared with traditional verification methods such as model checking,testing and theorem proving,runtime verification has the characteristics of low complexity and easy to operate,which is suitable for online verification of the WeChat system.At present,the research on the characteristics and properties of information spreading in the WeChat system mainly focuses on the hot spot mining and analysis in the WeChat public platform.There are few studies on the characteristics of information spreading and user behavior in the WeChat group.This thesis proposes an online runtime verification method of WeChat group based on three-valued propositional projection temporal logic(PPTL₃).First of all,by analyzing the official WeChat protocol and social network related laws and regulations,we get the properties that the WeChat group needs to satisfy when spreading information.Atomic propositions are defined according to properties and combined into PPTL₃ formulas for describing properties.The corresponding monitor of the formula is got by using the property monitor generation of PPTL property(PMG_PPTL),and the Java monitor generator reads the text file that saves the monitor information and builds the monitor in Java format.Then,we use the crawler to obtain the WeChat group data dynamically,analyze the properties that need to be verified and determine the relevant WeChat text.The special WeChat text is identified by text classification combining the word features,text format features,text semantic features and the automata algorithm based on keyword filtering,and values of atomic propositions are determined.Then,we combine atomic propositions into a state subformula representing the system path and input the subformula into the Java monitor.If the monitor reaches the true node,it indicates that the property is satisfied;if the monitor reaches the false node,it indicates that the property is unsatisfied;if the monitor reaches other nodes,it indicates that the information currently obtained cannot determine whether the property is satisfied or not,and the monitor needs to keep running.Finally,by comparing the runtime verification tool used in this thesis with other tools,the result shows the effectiveness of the tool used in verifying properties of WeChat group.