社交网络系统的建模与运行时验证

The runtime verification technique of SNS (Social Network Service) is investigated based on PTL (Projection Temporal Logic). The runtime trace of SNS is got by code instrumentation or web crawlers, and then the translator is constructed to build the formal MSVL (Modeling, Simulation and Verification Language) model for it. The MSVL program is used to describe the SNS desirable property, and the MSVL monitor is constructed to check the property. PPTL3 is defined by extending PPTL (Propositional PTL) with three-valued semantics, and it is also used to describe the SNS desirable property, then the PPTL3 monitor is constructed to check the property. The MSV platform is extended to support MSVL translator, MSVL monitor and PPTL3 monitor, so it can be applied for runtime verification of SNS.

在投影时序逻辑(Projection Temporal Logic, PTL)的框架下研究社交网络系统(Social Network Service, SNS)的运行时验证技术。研究SNS的建模方法：通过代码插桩或网络爬虫获取SNS的运行关键信息，构造转换工具建立SNS的MSVL(Modeling, Simulation and Verification Language)模型。研究SNS的性质描述方法：使用MSVL程序描述SNS的待验证性质，并研究MSVL监控器的构造方法；扩展PPTL(Propositional PTL)，定义三值时序逻辑PPTL3，使用PPTL3公式描述SNS的待验证性质，并研究PPTL3监控器的构造方法。扩展MSV平台以包含MSVL转换工具、MSVL监控器与PPTL3监控器，并应用于典型SNS实例的运行时验证。

社交网络系统（Social Network Service, SNS）是一群拥有相同兴趣与活动的人创建的在线社区，提供了便捷、低成本的交流方式，成为人们生活中不可或缺的一部分。但是SNS中存在用户隐私泄露、结构设计缺失、安全保障不足等问题，往往涉及大规模的社交用户，严重影响人们的日常生活。验证作为一种基于严格数学推理和证明的形式化方法，提供了一条保证SNS安全性和正确性的重要途径。在命题投影时序逻辑（Propositional Projection Temporal Logic, PPTL）语法及语义的基础上，建立三值语义逻辑PPTL3，使其语义除了真、假外，还包含不确定。定义其语义和逻辑规则，改进了PPTL的判定算法，给定公式的长度为L，公式中命题的集合为Φ，通过构建范式图确定算法的时间复杂度为O(L∗2^|Φ|)。该高效判定算法为后续的基于PPTL3的运行时验证奠定了基础。扩展了MSVL（Modeling, Simulation and Verification Language）语言，引入了指针类型、结构体类型以及相应的结构体指针类型。基于MSVL定义了Java、Python语言的形式化语义，给出了将Java、Python程序转换为MSVL程序的形式化规则。给出了PPTL3运行时验证监控器的构造方法，实现了监控器生成器。研究了若干典型的SNS场景，包括开源SNS，微博，微信等系统。基于隐马尔可夫模型和MSVL，研究了SNS的随机特性；通过代码插桩研究了开源SNS的在线运行时验证方法；将微博热点社会事件的特性描述为PPTL3公式，研究了微博热点社会事件的运行时检测方法；分析了微信群传播信息需要满足的性质，研究了微信群的在线运行时验证方法。