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

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

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

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

【部分圖文】：

圖4一1時鐘系統(tǒng)檢測

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

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

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

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

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



本文編號：3389521