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

【摘要】：形式化驗證方法(Formal Verification Method)是對軟硬件系統(tǒng)進行分析和驗證一種有效的方式。而模型檢測(Model Checking)技術(shù)是其中一種很重要的有限狀態(tài)系統(tǒng)自動驗證技術(shù),因其簡潔和自動化程度高的特征而備受關(guān)注。它主要用于分析驗證安全認證協(xié)議、通信協(xié)議、硬件檢測、控制系統(tǒng)等方面。模型檢測(Model Checking)是一種近年來比較流行的形式化驗證方法。目前有基于一階邏輯、高階邏輯、時態(tài)邏輯、自動機、狀態(tài)機等模型檢測技術(shù)。行為時序邏輯TLA(Temporal Logic of Actions)是由Leslie Lamport提出的一種新的邏輯,行為時序邏輯可以在一個程序中同時表達系統(tǒng)模型及系統(tǒng)屬性,使得系統(tǒng)形式化更為有效。目前,基于行為時序邏輯的模型檢測技術(shù)也是模型檢測的主流技術(shù)之一。它通過公式的形式在一種邏輯下同時表達系統(tǒng)模型與屬性。同時它具有自己的時序規(guī)約描述語言TLA+和對應的模型檢測工具TLC方便對用TLA+描述的并發(fā)系統(tǒng)模型進行檢測。因此,這種模型檢測技術(shù)具有重要的研究和利用價值。本文深入研究了模型檢測技術(shù)、自動機理論和行為時序邏輯TLA,行為時序邏輯的語言TLA+以及它的驗證工具TLC的結(jié)構(gòu)及使用方法.在詳細介紹網(wǎng)絡協(xié)議Pastry及其工作原理的基礎上,用TLA+對Pastry協(xié)議進行了分析建模同時用TLC進行了驗證分析,所作的主要工作與創(chuàng)新之處如下:(1)深入研究行為時序邏輯TLA,及其形式化語言TLA+,自動驗證工具TLC;(2)選取網(wǎng)絡協(xié)議pastry,并對其原理及其行為進行了詳細研究,分析了Join工作機制。(3)用TLA+語言對pastry協(xié)議進行建模及規(guī)約描述,通過TLC模型檢測工具對規(guī)約的系統(tǒng)進行驗證。
【關(guān)鍵詞】：網(wǎng)絡協(xié)議 pastry協(xié)議 模型檢測 TLA TLA+ TLC
【學位授予單位】：貴州大學
【學位級別】：碩士
【學位授予年份】：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
• 第二章 模型檢測與自動機理論12-25
• 2.1 形式化方法及模型檢測概述12-13
• 2.2 形式化方法過程13-14
• 2.3 自動機理論14-21
• 2.3.1 有限狀態(tài)自動機15-17
• 2.3.2 Büchi自動機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
• 第三章 行為時序邏輯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)絡及Pastry協(xié)議簡介37-38
• 4.2 Pastry協(xié)議節(jié)點數(shù)據(jù)結(jié)構(gòu)38-39
• 4.3 Pastry協(xié)議路由39-42
• 4.3.1 路由工作原理及算法描述39-42
• 4.4 Pastry協(xié)議的自組織和自適應42-44
• 4.4.1 Join42-44
• 4.4.2 Failure44
• 4.5 本章小結(jié)44-46
• 第五章 Pastry協(xié)議的規(guī)約描述與驗證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 驗證結(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
• 參考文獻63-67

【相似文獻】

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

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

2 謝揚光;同步時序邏輯網(wǎng)絡的圖上作業(yè)設計法[J];長春郵電學院學報;1986年02期

3 姜文彬;脈沖型時序邏輯網(wǎng)絡設計的解析方法[J];計算機學報;1989年04期

4 姜文彬;脈沖型時序邏輯網(wǎng)絡設計（Ⅲ）[J];山東建材學院學報;1995年02期

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

6 呂娜;;時序邏輯領域的開拓者[J];程序員;2009年12期

7 張春早;;時序邏輯設計的方格圖解法[J];湖北機械;1980年04期

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

9 姜文彬;脈沖型時序邏輯網(wǎng)絡分析[J];電子學報;1986年06期

10 曹立明,施潤身;基于時序邏輯的故障預測[J];上海鐵道大學學報;1998年12期

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

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

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

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

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

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

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

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

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

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

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

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

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

3 韓冰;線性時序邏輯在失業(yè)保險審計中的應用研究[D];哈爾濱工程大學;2010年

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

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

6 趙延珂;基于時序邏輯模型驗證的入侵檢測方法研究[D];鄭州大學;2014年

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

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

9 黃貽望;基于行為時序邏輯模型檢測的研究與應用[D];貴州大學;2009年

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

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

本文編號：358671