時序邏輯轉(zhuǎn)換斷言圖研究.pdf

1、由于因特網(wǎng)和嵌入式系統(tǒng)在汽車、飛機(jī)以及其它安全系統(tǒng)的成功應(yīng)用，未來將會更加依賴于計(jì)算機(jī)設(shè)備的功能。由于技術(shù)的快速發(fā)展，發(fā)展驗(yàn)證系統(tǒng)正確性的可靠方法變的越來越重要。目前用于復(fù)雜系統(tǒng)的有效方法包括仿真驗(yàn)證、測試驗(yàn)證和形式化驗(yàn)證。前兩者驗(yàn)證花費(fèi)的時間空間長、不易使用，并且無法做到對所有可能性輸入和潛在的缺陷進(jìn)行驗(yàn)證。形式化驗(yàn)證使用數(shù)學(xué)的方法證明給定的系統(tǒng)模型是否滿足要求，從而做到了對用例的全覆蓋。形式化驗(yàn)證又包括了形式化等價驗(yàn)證、推理驗(yàn)證和模

2、型驗(yàn)證。模型驗(yàn)證是一種用于驗(yàn)證有限狀態(tài)并發(fā)系統(tǒng)的技術(shù)，它對系統(tǒng)建模，并驗(yàn)證系統(tǒng)是否滿足規(guī)格說明。時序邏輯如 CTL、LTL是目前常用的規(guī)格說明語言，基于 CTL、LTL的模型檢驗(yàn)廣泛應(yīng)用于工業(yè)中。GSTE是一種高效的自動化模型檢驗(yàn)算法，使用斷言圖作為規(guī)格說明語言。斷言圖較時序邏輯更易于使用，而 LTL與斷言圖在描述方面更為接近，因此，將 LTL轉(zhuǎn)換成斷言圖有著實(shí)用的意義。
　　本課題從形式化方法的基本概念出發(fā)，對時序邏輯和斷言圖進(jìn)

3、行了對比其優(yōu)劣勢，并對斷言圖進(jìn)行了擴(kuò)展，針對課題進(jìn)一步的擴(kuò)展，提出了擴(kuò)展的驗(yàn)證算法，使得算法能夠驗(yàn)證擴(kuò)展之后的斷言圖并利用其性質(zhì)驗(yàn)證了算法的正確性和完備性。
　　本文首先介紹了形式化方法和模型檢驗(yàn)的概念，給出了課題的研究意義，其次詳細(xì)的介紹了廣義符號軌跡賦值的驗(yàn)證過程，引入了其規(guī)格說明語言斷言圖，再次本文介紹了LTL、CTL及基于這些時序邏輯的模型檢驗(yàn)算法，對比了CTL與LTL之間的區(qū)別和聯(lián)系，然后對比了 GSTE和基于時序邏輯的

4、模型驗(yàn)證算法，將時序邏輯轉(zhuǎn)換成 Büchi自動機(jī)，并將 Büchi自動機(jī)轉(zhuǎn)換成斷言圖，從而達(dá)到將時序邏輯轉(zhuǎn)換成 Büchi自動機(jī)的形式，在這過程中說明了斷言圖的局限性。本文基于廣義符號軌跡賦值的相關(guān)性質(zhì)引入終端的概念，基于斷言圖定義了終端斷言圖，并將強(qiáng)滿足算法進(jìn)行擴(kuò)展，提出終端可滿足性算法，使得其能驗(yàn)證終端斷言圖，本文給出了終端可滿足性的相關(guān)性質(zhì)，并使用數(shù)學(xué)推理證明了終端可滿足算法的正確性和完備性。在文章的最后，通過模型對性質(zhì)進(jìn)行驗(yàn)證滿