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

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

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

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

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