社交网络形式化建模与验证方法的实现

摘要

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

目录

第一个书签之前

摘要

ABSTRACT

插图索引

表格索引

符号对照表

缩略语对照表

第一章 绪论

1.1 研究背景

1.2 研究现状

1.2.1 社交网络的形式化研究

1.2.2 多社交网络研究

1.3 研究内容与组织结构

第二章 相关工作介绍

2.1 统一模型检测

2.2 社交网络隐私策略验证

2.3 本章小结

第三章 基于MSVL的社交网络建模与验证

3.1 方法框架

3.2 社交网络性质分类

3.3 社交网络数据获取

3.3.1 网络爬虫

3.3.2 数据获取过程

3.4 社交网络建模

3.4.1 SNS2MSVL工具

3.4.2 建模过程

3.5 多社交网络应用

3.5.1 用户身份识别

3.5.2 多社交网络建模

3.6 本章小节

第四章 社交网络建模与验证实例

4.1 单社交网络的建模与验证

4.1.1 单社交网络的性质获取

4.1.2 新浪微博的数据获取

4.1.3 性质的PPTL公式表示

4.1.4 MSVL模型的获取

4.1.5 性质验证

4.2 多社交网络的建模与验证

4.2.1 多社交网络的性质获取

4.2.2 QQ空间的数据获取

4.2.3 性质的PPTL公式表示

4.2.4 MSVL模型的获取

4.2.5 性质验证

4.3 与其它工具的比较

4.3.1 工具介绍

4.3.2 比较结果

4.4 本章小节

第五章 总结与展望

5.1 总结

5.2 展望

参考文献

附录A

附录B

致谢

作者简介

1. 基本情况

2. 教育背景

3. 攻读硕士学位期间的研究成果

3.1 发表学术论文

3.2 申请(授权)专利

3.3 参与科研项目及获奖