Runtime Verification Of Weibo System

With the development of computer technology and the advent of the Web2.0 era,especially the recent proposal of the Internet+concept,Internet applications have covered all aspects of people's lives.As a typical Internet application,the Social Network Service/Site?SNS?has penetrated into every corner of society and brought great convenience to people's lives and work.As one of the most popular social networking platforms,Weibo has gradually changed the way people access and share information for its low entry barriers,simple operation,high originality,and real-time characteristics.People can publish whatever they see and hear at any time and place in real-time,and spread this information quickly and widely with the forwarding and commentary mechanism of Weibo.But on the other hand,since the threshold for entry into Weibo is low,anyone can release any speech on it,and the speeches will spread freely on the Weibo platform,so the rumor is no exception.For example,the“salt crisis”in 2011 was spread rapidly on Weibo,which led to the salt price skyrocketing,and seriously affected people's daily life.Therefore,in order to focus on dynamic society better and guide social public opinion,the detection of hot social events of the Weibo platform is very necessary.At present,the detection of hot social events of Weibo is generally using the clustering method,but it needs to calculate the text similarity in the clustering process.When the Weibo data volume is large,the clustering efficiency will decrease.And after the clustering is completed,the extraction of the event abstract is needed.The selection of the abstract extraction algorithm will also affect the accuracy of the event detection.Therefore,this thesis proposes a runtime verification method based on three-value Propositional Projection Temporal Logic?PPTL?PPTL₃ to detect hot social events in Weibo.In the method,firstly,the characteristic of hot social event in Weibo is studied to get its unique properties,and define the corresponding atomic propositions,then the atomic propositions are combined to get the PPTL₃ formula describing the property,and the monitor of the property is built.Then,the Weibo data is crawled by a web crawler and the required information is extracted into a file.After that the Weibo data files are read in turn,and the truth values of the atomic propositions are determined according to the Weibo data in each file;then atomic propositions with truth value are combined into a state formula which represents the system trace,as the input of the monitor,and according to the output of the monitor,the hot social events are obtained.Finally,the effectiveness of this method is tested by comparing it with three commonly used event detection methods,including single-pass,HAC and K-means,using the actual Sina Weibo data.The experimental results show that this method can effectively detect some hot social events in Weibo.