基于行為時序邏輯模型檢測的研究與應用.pdf

1、模型檢測是一種基于形式化方法的自動分析和驗證技術，問題的關鍵是狀態(tài)空間爆炸的解決。Lesilie Lamport提出行為時序邏輯（TLA）理論體系，運用TLA對軟件或協(xié)議進行建模，它能在一種語言中同時表達程序與屬性，在理論和實際應用中，這種模型檢測技術具有一定研究價值。
　　本文在詳細介紹行為時序邏輯基本概念的基礎上，分析了使用行為時序邏輯基本理論對并發(fā)系統(tǒng)的建模，運用TLA+規(guī)約語言與檢測工具對并發(fā)系統(tǒng)和網(wǎng)絡安全協(xié)議進行簡要分析

2、與檢測，所作的主要工作與創(chuàng)新之處如下：
　　1、在行為時序邏輯（Temporal Logic of Action）的基礎上嚴格定義了行為
　　路徑對行動的強弱公平性，并詳細證明了并發(fā)系統(tǒng)中行為對行動的強弱公平性，介紹 TLA語法與語義，并分析TLA的邏輯推理規(guī)則，以簡單程序?qū)嵗治龊妥C明并發(fā)系統(tǒng)所具有的不變性，對程序的不同 TLA時序公式之間等價性進行分析；
　　2、TLA+是基于TLA的描述并發(fā)系統(tǒng)的規(guī)約語言，闡述了

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