论文部分内容阅读
随着信息化时代的到来,社交网络应运而生,它为人们提供了便捷、低成本的交流方式,成为人们生活中不可或缺的一部分。由于社交网络中存在用户隐私泄露、结构设计缺失、安全保障不足等问题,而验证社交网络的相关性质可以完善其隐私策略、优化其结构设计、提高其安全性等,因此社交网络的验证成为计算机领域的热门研究课题。形式化验证方法用逻辑推理对软硬件、系统设计等进行验证,判断它们是否符合相关的规范要求。目前较为常见的形式化验证方法有:定理证明,模型检测等,它们在建模社交网络,验证相关性质等方面得到了应用。大部分形式化方法通过分析多个典型社交网络的共有特性来人工地进行社交网络建模,较少运用自动化工具。这些方法主要对某一特定性质进行验证,缺乏总体上的性质共性分析和分类。此外,它们的主要研究对象是单个社交网络,对多社交网络的研究较少。针对上述情况,本文提出了一种基于时序逻辑程序设计语言(Modeling,Simulation and Verification Language,MSVL)的社交网络形式化建模与验证的实现方法。本方法以特定社交网络的性质研究作为驱动,其流程可以概括为:首先,对社交网络的性质进行分类,将其分为隐私策略,用户行为以及社会属性三个方面;然后,针对特定社交网络,根据性质分类来选取具有代表性的性质并用命题投影时序逻辑(Propositional Projection Temporal Logic,PPTL)公式进行表示;其次,通过网络爬虫获取与性质相关的特定社交网络数据,分析提取后将其保存为XML文件,并使用工具SNS2MSVL将XML文件转换成MSVL程序,实现对社交网络的半自动化建模;最后,将性质的PPTL公式和模型的MSVL程序输入到MSVL编译器中,进行建模,仿真以及验证。针对综合类社交网络新浪微博和QQ空间,实现了社交网络形式化建模与验证的两个实例:新浪微博的单社交网络实例,新浪微博和QQ空间的多社交网络实例,实验结果表明了本方法的可行性。通过和其它的形式化验证工具进行比较,表明本方法在社交网络形式化建模与验证的效率、健壮性以及代码规模方面具有一定的优势。