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

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

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

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

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