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

发布时间：2021-08-25 02:45

　　随着信息化时代的到来,社交网络应运而生,它为人们提供了便捷、低成本的交流方式,成为人们生活中不可或缺的一部分。由于社交网络中存在用户隐私泄露、结构设计缺失、安全保障不足等问题,而验证社交网络的相关性质可以完善其隐私策略、优化其结构设计、提高其安全性等,因此社交网络的验证成为计算机领域的热门研究课题。形式化验证方法用逻辑推理对软硬件、系统设计等进行验证,判断它们是否符合相关的规范要求。目前较为常见的形式化验证方法有:定理证明,模型检测等,它们在建模社交网络,验证相关性质等方面得到了应用。大部分形式化方法通过分析多个典型社交网络的共有特性来人工地进行社交网络建模,较少运用自动化工具。这些方法主要对某一特定性质进行验证,缺乏总体上的性质共性分析和分类。此外,它们的主要研究对象是单个社交网络,对多社交网络的研究较少。针对上述情况,本文提出了一种基于时序逻辑程序设计语言（Modeling,Simulation and Verification Language,MSVL）的社交网络形式化建模与验证的实现方法。本方法以特定社交网络的性质研究作为驱动,其流程可以概括为:首先,对社交网络的性质进行分类... 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：77 页

【学位级别】：硕士

【部分图文】：

新浪微博14-17年的月活跃用户增长统计图

西安电子科技大学硕士学位论文图2.2MC 的流程图MC 具有以下三种功能：1. 建模，通过执行用户输入的 MSVL 程序，MC 能够找到该程序所能生出的所有形式化模型，并给出由范式图(Normal Form Graph, NFG)表示的包含状态结点和状态转移的边的状态序列，也就是建模结果。MC 同时会生成出 Output.txt文件用来记录状态序列中状态结点和边的信息以及建模所需的时间。2. 仿真，通过执行用 MSVL 语言描述的模型程序，得到其所对应状态序列。如果状态执行为真，那么 MC 就会找到程序的一个模型

第三章 基于 MSVL 的社交网络建模与验证ct relationship{ //社交网络的用户关系链表g Id //该社交网络的用户关系中关联的用户 ID//根据不同社交网络特点所衍生的关系信息tionship *next； //该社交网络的用户关系的链表指针S2MSVL 工具的界面如图 3.7 所示，分为单社交网络建模（图中的项），以及多社交网络建模（图中的“多 SNS 建模”选项）。


本文编号：3361230