模型檢測(cè)是一種基于形式化方法的自動(dòng)分析和驗(yàn)證技術(shù),問(wèn)題的關(guān)鍵是狀態(tài)空間爆炸的解決。Lesilie Lamport提出行為時(shí)序邏輯（TLA）理論體系,運(yùn)用TLA對(duì)軟件或協(xié)議進(jìn)行建模,它能在一種語(yǔ)言中同時(shí)表達(dá)程序與屬性,在理論和實(shí)際應(yīng)用中,這種模型檢測(cè)技術(shù)具有一定研究?jī)r(jià)值。本文在詳細(xì)介紹行為時(shí)序邏輯基本概念的基礎(chǔ)上,分析了使用行為時(shí)序邏輯基本理論對(duì)并發(fā)系統(tǒng)的建模,運(yùn)用TLA+規(guī)約語(yǔ)言與檢測(cè)工具對(duì)并發(fā)系統(tǒng)和網(wǎng)絡(luò)安全協(xié)議進(jìn)行簡(jiǎn)要分析與檢測(cè),所作的主要工作與創(chuàng)新之處如下:1、在行為時(shí)序邏輯（Temporal Logic of Action）的基礎(chǔ)上嚴(yán)格定義了行為路徑對(duì)行動(dòng)的強(qiáng)弱公平性,并詳細(xì)證明了并發(fā)系統(tǒng)中行為對(duì)行動(dòng)的強(qiáng)弱公平性,介紹TLA語(yǔ)法與語(yǔ)義,并分析TLA的邏輯推理規(guī)則,以簡(jiǎn)單程序?qū)嵗治龊妥C明并發(fā)系統(tǒng)所具有的不變性,對(duì)程序的不同TLA時(shí)序公式之間等價(jià)性進(jìn)行分析;2、TLA+是基于TLA的描述并發(fā)系統(tǒng)的規(guī)約語(yǔ)言,闡述了使用TLA+語(yǔ)言描述并發(fā)系統(tǒng)的規(guī)約方法,分析檢測(cè)工具TLC的結(jié)構(gòu)組成、各命令參數(shù)的功能及檢測(cè)原理及要求,研究了協(xié)議的分析、建模及檢測(cè)流程;3、基于TLA的網(wǎng)絡(luò)協(xié)議與并發(fā)系統(tǒng)... 

【文章來(lái)源】：貴州大學(xué)貴州省 211工程院校

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

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

【部分圖文】：

圖4一1時(shí)鐘系統(tǒng)檢測(cè)

用Generato:進(jìn)行隨機(jī)模擬。在dos命令符下鍵入 javatle.GeneratorHourCloek.tla，運(yùn)行類Generator模塊，如下圖是簡(jiǎn)單的時(shí)釗，規(guī)約系統(tǒng)檢測(cè):圖4一1時(shí)鐘系統(tǒng)檢測(cè)結(jié)果顯示:沒(méi)有檢測(cè)出錯(cuò)誤，生成24個(gè)狀態(tài)，12個(gè)可區(qū)分狀態(tài)，計(jì)算狀態(tài)深度為1。對(duì)時(shí)鐘系統(tǒng)描述文件進(jìn)行隨機(jī)模擬，dos命令符下鍵入 javatlc.GeneratorHourCloek.tla，運(yùn)行類Generator模塊，如下圖所示:圖4一2時(shí)序系統(tǒng)隨機(jī)模擬生成默認(rèn)十條狀態(tài)數(shù)為10的運(yùn)行軌跡文件，其中兩條軌跡分別如下所示: HourCloekZtraeel:圖4一3時(shí)序系統(tǒng)軌跡(l)

用Generato:進(jìn)行隨機(jī)模擬。在dos命令符下鍵入 javatle.GeneratorHourCloek.tla，運(yùn)行類Generator模塊，如下圖是簡(jiǎn)單的時(shí)釗，規(guī)約系統(tǒng)檢測(cè):圖4一1時(shí)鐘系統(tǒng)檢測(cè)結(jié)果顯示:沒(méi)有檢測(cè)出錯(cuò)誤，生成24個(gè)狀態(tài)，12個(gè)可區(qū)分狀態(tài)，計(jì)算狀態(tài)深度為1。對(duì)時(shí)鐘系統(tǒng)描述文件進(jìn)行隨機(jī)模擬，dos命令符下鍵入 javatlc.GeneratorHourCloek.tla，運(yùn)行類Generator模塊，如下圖所示:圖4一2時(shí)序系統(tǒng)隨機(jī)模擬生成默認(rèn)十條狀態(tài)數(shù)為10的運(yùn)行軌跡文件，其中兩條軌跡分別如下所示: HourCloekZtraeel:圖4一3時(shí)序系統(tǒng)軌跡(l)

【參考文獻(xiàn)】：
期刊論文
[1]安全協(xié)議形式化混合分析技術(shù)的研究與應(yīng)用[J]. 付宇,馬自堂,王惠芳.  計(jì)算機(jī)工程. 2006(17)
[2]基于SMV的網(wǎng)絡(luò)協(xié)議形式化分析與驗(yàn)證[J]. 文靜華,余濱,張梅,李祥.  計(jì)算機(jī)工程. 2006(15)
[3]基于TLA+的BRP協(xié)議規(guī)約及驗(yàn)證[J]. 陳立前,王戟,陳火旺.  計(jì)算機(jī)工程與科學(xué). 2006(01)
[4]密碼協(xié)議的Promela語(yǔ)言建模及分析[J]. 龍士工,王巧麗,李祥.  計(jì)算機(jī)應(yīng)用. 2005(07)
[5]一種電子商務(wù)協(xié)議原子性的模型檢驗(yàn)分析方法[J]. 董榮勝,郭云川,古天龍.  計(jì)算機(jī)科學(xué). 2005(04)
[6]密碼協(xié)議的符號(hào)模型檢測(cè)及分析[J]. 龍士工,羅文俊,李祥.  計(jì)算機(jī)應(yīng)用. 2005(01)
[7]基于有窮自動(dòng)機(jī)模型的電子商務(wù)支付協(xié)議公平性研究[J]. 謝曉堯,張煥國(guó).  計(jì)算機(jī)應(yīng)用. 2004(06)
[8]模型檢測(cè):理論、方法與應(yīng)用[J]. 林惠民,張文輝.  電子學(xué)報(bào). 2002(S1)
[9]基于時(shí)序邏輯的加密協(xié)議分析[J]. 肖德琴,周權(quán),張煥國(guó),劉才興.  計(jì)算機(jī)學(xué)報(bào). 2002(10)
[10]Needham-Schroeder公鑰協(xié)議的模型檢測(cè)分析[J]. 張玉清,王磊,肖國(guó)鎮(zhèn),吳建平.  軟件學(xué)報(bào). 2000(10)

博士論文
[1]界程演算模型檢測(cè)[D]. 江華.貴州大學(xué) 2008

碩士論文
[1]SPIN模型檢測(cè)的研究與應(yīng)用[D]. 王巧麗.貴州大學(xué) 2006



本文編號(hào)：3389521