基于行為時(shí)序邏輯模型檢測(cè)的研究與應(yīng)用.pdf

1、模型檢測(cè)是一種基于形式化方法的自動(dòng)分析和驗(yàn)證技術(shù)，問題的關(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)要分析

2、與檢測(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ǔ)言，闡述了

3、使用TLA+語(yǔ)言描述并發(fā)系統(tǒng)的規(guī)約方法，分析檢測(cè)工具 TLC的結(jié)構(gòu)組成、各命令參數(shù)的功能及檢測(cè)原理及要求，研究了協(xié)議的分析、建模及檢測(cè)流程；
　　3、基于TLA的網(wǎng)絡(luò)協(xié)議與并發(fā)系統(tǒng)模型的形式化建模、分析與檢測(cè)，以時(shí)鐘并發(fā)系統(tǒng)為實(shí)例進(jìn)行TLA+建模與分析，并給出系統(tǒng)所需滿足的一些基本性質(zhì)的TLA時(shí)序公式，通過 TLC工具檢測(cè)，系統(tǒng)滿足這些屬性；
　　4、提出使用基于TLA對(duì)網(wǎng)絡(luò)安全協(xié)議分析與檢測(cè)的分析與研究，對(duì) NS協(xié)議進(jìn)行形