隨著信息化時(shí)代的到來(lái),社交網(wǎng)絡(luò)應(yīng)運(yùn)而生,它為人們提供了便捷、低成本的交流方式,成為人們生活中不可或缺的一部分。由于社交網(wǎng)絡(luò)中存在用戶隱私泄露、結(jié)構(gòu)設(shè)計(jì)缺失、安全保障不足等問(wèn)題,而驗(yàn)證社交網(wǎng)絡(luò)的相關(guān)性質(zhì)可以完善其隱私策略、優(yōu)化其結(jié)構(gòu)設(shè)計(jì)、提高其安全性等,因此社交網(wǎng)絡(luò)的驗(yàn)證成為計(jì)算機(jī)領(lǐng)域的熱門(mén)研究課題。形式化驗(yàn)證方法用邏輯推理對(duì)軟硬件、系統(tǒng)設(shè)計(jì)等進(jìn)行驗(yàn)證,判斷它們是否符合相關(guān)的規(guī)范要求。目前較為常見(jiàn)的形式化驗(yàn)證方法有:定理證明,模型檢測(cè)等,它們?cè)诮Ｉ缃痪W(wǎng)絡(luò),驗(yàn)證相關(guān)性質(zhì)等方面得到了應(yīng)用。大部分形式化方法通過(guò)分析多個(gè)典型社交網(wǎng)絡(luò)的共有特性來(lái)人工地進(jìn)行社交網(wǎng)絡(luò)建模,較少運(yùn)用自動(dòng)化工具。這些方法主要對(duì)某一特定性質(zhì)進(jìn)行驗(yàn)證,缺乏總體上的性質(zhì)共性分析和分類(lèi)。此外,它們的主要研究對(duì)象是單個(gè)社交網(wǎng)絡(luò),對(duì)多社交網(wǎng)絡(luò)的研究較少。針對(duì)上述情況,本文提出了一種基于時(shí)序邏輯程序設(shè)計(jì)語(yǔ)言（Modeling,Simulation and Verification Language,MSVL）的社交網(wǎng)絡(luò)形式化建模與驗(yàn)證的實(shí)現(xiàn)方法。本方法以特定社交網(wǎng)絡(luò)的性質(zhì)研究作為驅(qū)動(dòng),其流程可以概括為:首先,對(duì)社交網(wǎng)絡(luò)的性質(zhì)進(jìn)行分類(lèi)... 

【文章來(lái)源】：西安電子科技大學(xué)陜西省 211工程院校 教育部直屬院校

【文章頁(yè)數(shù)】：77 頁(yè)

【學(xué)位級(jí)別】：碩士

【部分圖文】：

新浪微博14-17年的月活躍用戶增長(zhǎng)統(tǒng)計(jì)圖

西安電子科技大學(xué)碩士學(xué)位論文圖2.2MC 的流程圖MC 具有以下三種功能：1. 建模，通過(guò)執(zhí)行用戶輸入的 MSVL 程序，MC 能夠找到該程序所能生出的所有形式化模型，并給出由范式圖(Normal Form Graph, NFG)表示的包含狀態(tài)結(jié)點(diǎn)和狀態(tài)轉(zhuǎn)移的邊的狀態(tài)序列，也就是建模結(jié)果。MC 同時(shí)會(huì)生成出 Output.txt文件用來(lái)記錄狀態(tài)序列中狀態(tài)結(jié)點(diǎn)和邊的信息以及建模所需的時(shí)間。2. 仿真，通過(guò)執(zhí)行用 MSVL 語(yǔ)言描述的模型程序，得到其所對(duì)應(yīng)狀態(tài)序列。如果狀態(tài)執(zhí)行為真，那么 MC 就會(huì)找到程序的一個(gè)模型

第三章 基于 MSVL 的社交網(wǎng)絡(luò)建模與驗(yàn)證ct relationship{ //社交網(wǎng)絡(luò)的用戶關(guān)系鏈表g Id //該社交網(wǎng)絡(luò)的用戶關(guān)系中關(guān)聯(lián)的用戶 ID//根據(jù)不同社交網(wǎng)絡(luò)特點(diǎn)所衍生的關(guān)系信息tionship *next； //該社交網(wǎng)絡(luò)的用戶關(guān)系的鏈表指針S2MSVL 工具的界面如圖 3.7 所示，分為單社交網(wǎng)絡(luò)建模（圖中的項(xiàng)），以及多社交網(wǎng)絡(luò)建模（圖中的“多 SNS 建�！边x項(xiàng)）。


本文編號(hào)：3361230