本文關(guān)鍵詞：基于行為時(shí)序邏輯TLA的網(wǎng)絡(luò)協(xié)議的描述與驗(yàn)證，由筆耕文化傳播整理發(fā)布。

【摘要】：形式化驗(yàn)證方法(Formal Verification Method)是對軟硬件系統(tǒng)進(jìn)行分析和驗(yàn)證一種有效的方式。而模型檢測(Model Checking)技術(shù)是其中一種很重要的有限狀態(tài)系統(tǒng)自動(dòng)驗(yàn)證技術(shù),因其簡潔和自動(dòng)化程度高的特征而備受關(guān)注。它主要用于分析驗(yàn)證安全認(rèn)證協(xié)議、通信協(xié)議、硬件檢測、控制系統(tǒng)等方面。模型檢測(Model Checking)是一種近年來比較流行的形式化驗(yàn)證方法。目前有基于一階邏輯、高階邏輯、時(shí)態(tài)邏輯、自動(dòng)機(jī)、狀態(tài)機(jī)等模型檢測技術(shù)。行為時(shí)序邏輯TLA(Temporal Logic of Actions)是由Leslie Lamport提出的一種新的邏輯,行為時(shí)序邏輯可以在一個(gè)程序中同時(shí)表達(dá)系統(tǒng)模型及系統(tǒng)屬性,使得系統(tǒng)形式化更為有效。目前,基于行為時(shí)序邏輯的模型檢測技術(shù)也是模型檢測的主流技術(shù)之一。它通過公式的形式在一種邏輯下同時(shí)表達(dá)系統(tǒng)模型與屬性。同時(shí)它具有自己的時(shí)序規(guī)約描述語言TLA+和對應(yīng)的模型檢測工具TLC方便對用TLA+描述的并發(fā)系統(tǒng)模型進(jìn)行檢測。因此,這種模型檢測技術(shù)具有重要的研究和利用價(jià)值。本文深入研究了模型檢測技術(shù)、自動(dòng)機(jī)理論和行為時(shí)序邏輯TLA,行為時(shí)序邏輯的語言TLA+以及它的驗(yàn)證工具TLC的結(jié)構(gòu)及使用方法.在詳細(xì)介紹網(wǎng)絡(luò)協(xié)議Pastry及其工作原理的基礎(chǔ)上,用TLA+對Pastry協(xié)議進(jìn)行了分析建模同時(shí)用TLC進(jìn)行了驗(yàn)證分析,所作的主要工作與創(chuàng)新之處如下:(1)深入研究行為時(shí)序邏輯TLA,及其形式化語言TLA+,自動(dòng)驗(yàn)證工具TLC;(2)選取網(wǎng)絡(luò)協(xié)議pastry,并對其原理及其行為進(jìn)行了詳細(xì)研究,分析了Join工作機(jī)制。(3)用TLA+語言對pastry協(xié)議進(jìn)行建模及規(guī)約描述,通過TLC模型檢測工具對規(guī)約的系統(tǒng)進(jìn)行驗(yàn)證。
【關(guān)鍵詞】：網(wǎng)絡(luò)協(xié)議 pastry協(xié)議 模型檢測 TLA TLA+ TLC
【學(xué)位授予單位】：貴州大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：TP306
【目錄】：

• 摘要5-6
• ABSTRACT6-8
• 第一章 引言8-12
• 1.1 研究背景及意義8-9
• 1.2 國內(nèi)外研究現(xiàn)狀及存在的問題9-10
• 1.3 論文的主要研究工作及創(chuàng)新10
• 1.4 論文的結(jié)構(gòu)安排10-12
• 第二章 模型檢測與自動(dòng)機(jī)理論12-25
• 2.1 形式化方法及模型檢測概述12-13
• 2.2 形式化方法過程13-14
• 2.3 自動(dòng)機(jī)理論14-21
• 2.3.1 有限狀態(tài)自動(dòng)機(jī)15-17
• 2.3.2 Büchi自動(dòng)機(jī)17-19
• 2.3.3 語言判空19-21
• 2.4 模型檢測原理、過程方法21-23
• 2.4.1 模型檢測原理21-22
• 2.4.2 模型檢測的過程22-23
• 2.5 本章小結(jié)23-25
• 第三章 行為時(shí)序邏輯TLA25-37
• 3.1 概述25
• 3.2 TLA的基本概念25-29
• 3.2.1 符號與語法27-28
• 3.2.2 行為與語義28-29
• 3.3 TLA中的公平性、活性、安全性29-31
• 3.3.1 公平性29-30
• 3.3.2 活性30
• 3.3.5 安全性30-31
• 3.4 TLA+語言31-34
• 3.4.1 TLA+模塊31
• 3.4.2 TLA+操作符31-34
• 3.5 TLC模型檢測器34-36
• 3.6 本章小結(jié)36-37
• 第四章 Pastry協(xié)議37-46
• 4.1 P2P網(wǎng)絡(luò)及Pastry協(xié)議簡介37-38
• 4.2 Pastry協(xié)議節(jié)點(diǎn)數(shù)據(jù)結(jié)構(gòu)38-39
• 4.3 Pastry協(xié)議路由39-42
• 4.3.1 路由工作原理及算法描述39-42
• 4.4 Pastry協(xié)議的自組織和自適應(yīng)42-44
• 4.4.1 Join42-44
• 4.4.2 Failure44
• 4.5 本章小結(jié)44-46
• 第五章 Pastry協(xié)議的規(guī)約描述與驗(yàn)證46-60
• 5.1 Pastry協(xié)議形式化規(guī)約過程分析46-47
• 5.2 Pastry協(xié)議的規(guī)約描述47-55
• 5.2.1 定義、常量、變量和消息類型47-49
• 5.2.2 協(xié)議接.間的行為描述規(guī)約49-51
• 5.2.3 協(xié)議內(nèi)部的行為描述規(guī)約51-54
• 5.2.4 下一狀態(tài)關(guān)系描述54-55
• 5.3 Pastry協(xié)議中的性質(zhì)描述55
• 5.4 驗(yàn)證結(jié)果與分析55-58
• 5.5 結(jié)論58-59
• 5.6 本章小結(jié)59-60
• 第六章 總結(jié)與展望60-62
• 6.1 主要工作總結(jié)60
• 6.2 展望60-62
• 致謝62-63
• 參考文獻(xiàn)63-67

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

1 黃佳;;基于行為時(shí)序邏輯的安全協(xié)議研究[J];信息通信;2012年04期

2 謝揚(yáng)光;同步時(shí)序邏輯網(wǎng)絡(luò)的圖上作業(yè)設(shè)計(jì)法[J];長春郵電學(xué)院學(xué)報(bào);1986年02期

3 姜文彬;脈沖型時(shí)序邏輯網(wǎng)絡(luò)設(shè)計(jì)的解析方法[J];計(jì)算機(jī)學(xué)報(bào);1989年04期

4 姜文彬;脈沖型時(shí)序邏輯網(wǎng)絡(luò)設(shè)計(jì)（Ⅲ）[J];山東建材學(xué)院學(xué)報(bào);1995年02期

5 賈國平,鄭國梁;用于反應(yīng)系統(tǒng)的修改時(shí)序邏輯[J];軟件學(xué)報(bào);1997年09期

6 呂娜;;時(shí)序邏輯領(lǐng)域的開拓者[J];程序員;2009年12期

7 張春早;;時(shí)序邏輯設(shè)計(jì)的方格圖解法[J];湖北機(jī)械;1980年04期

8 馮玉琳;林惠民;唐稚松;;時(shí)序邏輯程序的證明系統(tǒng)[J];計(jì)算機(jī)研究與發(fā)展;1985年10期

9 姜文彬;脈沖型時(shí)序邏輯網(wǎng)絡(luò)分析[J];電子學(xué)報(bào);1986年06期

10 曹立明,施潤身;基于時(shí)序邏輯的故障預(yù)測[J];上海鐵道大學(xué)學(xué)報(bào);1998年12期

中國重要會(huì)議論文全文數(shù)據(jù)庫 前3條

1 章超;李彩虹;李廉;;SPIN在同步時(shí)序邏輯中的應(yīng)用[A];2005年全國理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2005年

2 馮荷飛;曹子寧;;交錯(cuò)時(shí)序認(rèn)知邏輯在安全協(xié)議中的應(yīng)用[A];邏輯學(xué)及其應(yīng)用研究——第四屆全國邏輯系統(tǒng)、智能科學(xué)與信息科學(xué)學(xué)術(shù)會(huì)議論文集[C];2008年

3 吳彪;朱立新;趙佳;;基于CPLD的可編程并行接口芯片8255設(shè)計(jì)與仿真[A];系統(tǒng)仿真技術(shù)及其應(yīng)用（第7卷）——'2005系統(tǒng)仿真技術(shù)及其應(yīng)用學(xué)術(shù)交流會(huì)論文選編[C];2005年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前5條

1 劉萬偉;擴(kuò)展時(shí)序邏輯的推理及符號化模型檢驗(yàn)技術(shù)[D];國防科學(xué)技術(shù)大學(xué);2009年

2 楊琛;打結(jié)不變的命題投影時(shí)序邏輯與模型檢測[D];西安電子科技大學(xué);2010年

3 萬良;基于行為時(shí)序邏輯TLA的系統(tǒng)、規(guī)則與協(xié)議檢測的研究[D];貴州大學(xué);2009年

4 張南;命題投影時(shí)序邏輯的完備公理系統(tǒng)與形式驗(yàn)證[D];西安電子科技大學(xué);2012年

5 趙常智;基于運(yùn)行時(shí)驗(yàn)證的軟件監(jiān)控關(guān)鍵技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2011年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 張麗;命題投影時(shí)序邏輯的判定性和表達(dá)性[D];西安電子科技大學(xué);2007年

2 楊琳琳;基于時(shí)序邏輯的安全協(xié)議驗(yàn)證方法的研究[D];南京航空航天大學(xué);2010年

3 韓冰;線性時(shí)序邏輯在失業(yè)保險(xiǎn)審計(jì)中的應(yīng)用研究[D];哈爾濱工程大學(xué);2010年

4 田聰;命題投影時(shí)序邏輯的可判定性[D];西安電子科技大學(xué);2007年

5 林麗秀;時(shí)序邏輯轉(zhuǎn)換斷言圖的研究[D];電子科技大學(xué);2013年

6 趙延珂;基于時(shí)序邏輯模型驗(yàn)證的入侵檢測方法研究[D];鄭州大學(xué);2014年

7 李亞利;基于可能性測度的時(shí)序邏輯性質(zhì)研究[D];陜西師范大學(xué);2013年

8 葛徐駿;基于時(shí)序邏輯的雙向一致性檢測[D];華東師范大學(xué);2015年

9 黃貽望;基于行為時(shí)序邏輯模型檢測的研究與應(yīng)用[D];貴州大學(xué);2009年

10 劉照洋;基于行為時(shí)序邏輯TLA的網(wǎng)絡(luò)協(xié)議的描述與驗(yàn)證[D];貴州大學(xué);2015年

  本文關(guān)鍵詞：基于行為時(shí)序邏輯TLA的網(wǎng)絡(luò)協(xié)議的描述與驗(yàn)證，，由筆耕文化傳播整理發(fā)布。

本文編號：358671