21195.有效模型檢測(cè)算法與安全性檢測(cè)

1、貴州大學(xué)2015屆碩士研究生學(xué)位論文有效模型檢測(cè)算法與安全性檢測(cè)學(xué)科專業(yè)：應(yīng)用數(shù)學(xué)研究方向：密碼學(xué)理論與工程導(dǎo)師：龍士工教授研究生：張鐸中國(guó)﹒貴州﹒貴陽(yáng)2015年5月分類號(hào)：TP301論文編號(hào)：201501031617密級(jí)：公開(kāi)貴州大學(xué)碩士學(xué)位論文I有效模型檢測(cè)算法與安全性檢測(cè)有效模型檢測(cè)算法與安全性檢測(cè)摘要隨著信息技術(shù)和網(wǎng)絡(luò)技術(shù)的迅速發(fā)展，計(jì)算機(jī)網(wǎng)絡(luò)在日常生活中的應(yīng)用日益普遍.如何確保其正確性和安全性成為日益緊迫的問(wèn)題.在現(xiàn)有的諸多理

2、論和方法中，模型檢測(cè)以其簡(jiǎn)潔明了和自動(dòng)化程度高的特點(diǎn)而受人關(guān)注.以色列學(xué)者伯努利將時(shí)序邏輯引入計(jì)算機(jī)科學(xué)，把它作為系統(tǒng)建模和驗(yàn)證工具取得了非常大的成功，絕大部分以線性時(shí)序邏輯為基礎(chǔ)的模型檢測(cè)技術(shù)都是基于自動(dòng)機(jī)理論實(shí)現(xiàn)的.本文在詳細(xì)介紹了線性時(shí)序邏輯（LinearTempalLogic簡(jiǎn)稱LTL）和自動(dòng)機(jī)理論的基礎(chǔ)上，分析了線性時(shí)序邏輯在建模規(guī)約中的可行性；研究了線性時(shí)序邏輯公式轉(zhuǎn)化為自動(dòng)機(jī)的具體算法；引入了集合論中勢(shì)的概念重點(diǎn)討論了安全

3、性的各種形式化定義以及等價(jià)性證明.所作的主要工作如下：1、結(jié)合模型檢測(cè)和自動(dòng)機(jī)理論，重點(diǎn)研究了非確定性自動(dòng)機(jī)（NFA）轉(zhuǎn)化為確定性自動(dòng)機(jī)（DFA）的方法和原理以及Bchi自動(dòng)機(jī)的合并和空集的檢測(cè).2、將自動(dòng)機(jī)理論與模型檢測(cè)原理相結(jié)合，研究了基于線性時(shí)序邏輯（LTL）下的模型檢測(cè)，設(shè)計(jì)了LTL轉(zhuǎn)化為自動(dòng)機(jī)的具體算法并分析了算法的正確性和優(yōu)越性.3、基于安全性的各種形式化定義，引入了集合論中勢(shì)的概念證明了不同定義之間的等價(jià)關(guān)系并結(jié)合自動(dòng)機(jī)的