基于矩陣半張量積模型檢測算法的研究與實現(xiàn).pdf

1、在計算機科學(xué)迅猛發(fā)展的今天，云計算、物聯(lián)網(wǎng)、移動互聯(lián)網(wǎng)成了時代的標(biāo)志，這些軟件技術(shù)的高速發(fā)展對自身驗證的可靠性和硬件性能提出了挑戰(zhàn)，對于硬件的性能要求最終落到了硬件集成電路的可靠性上面。然而，在硬件發(fā)展的歷程中，驗證集成芯片的正確性和可靠性一直是一個瓶頸。在驗證領(lǐng)域使用最多的是基于模擬的驗證方式，這種檢驗方式存在其不可彌補的缺點，即它只能證明系統(tǒng)有錯，而不能證明系統(tǒng)設(shè)計的正確性。而在軟件方面，對于可靠性的驗證還處于沒有形成特定規(guī)范的階段

2、。所以無論是針對軟件還是硬件，對其可靠性的驗證都是有實質(zhì)意義的。
　　本文主要以半張量積為數(shù)學(xué)理論，研究一種基于半張量積的模型檢測算法。算法主要分為三個部分：被驗證系統(tǒng)的數(shù)學(xué)建模、被驗證系統(tǒng)需要滿足的屬性描述和模型檢測算法。
　　針對被驗證系統(tǒng)數(shù)學(xué)建模，首先根據(jù)被驗證系統(tǒng)的原子集合，固定原子公式順序，考查原子公式的取值，確定原子公式在系統(tǒng)狀態(tài)的取值情況，定義系統(tǒng)狀態(tài)的布爾編碼表示。然后使用矩陣半張量積的邏輯抽象方法對系統(tǒng)狀態(tài)

3、向量化，得到系統(tǒng)的狀態(tài)向量。根據(jù)規(guī)定系統(tǒng)狀態(tài)的順序，利用圖論的鄰接矩陣定義被驗證系統(tǒng)的結(jié)構(gòu)矩陣。最后使用向量乘法描述系統(tǒng)運行狀態(tài)，并給出模型檢測算法的正確性和有窮性的數(shù)學(xué)證明。
　　本算法對被檢測的屬性的描述采用分支時態(tài)邏輯的計算樹邏輯，因此分析了計算樹邏輯（Computation Tree Logic，CTL）的適當(dāng)集，選取相應(yīng)的適當(dāng)集對任意CTL公式進(jìn)行標(biāo)準(zhǔn)化描述。針對CTL的適當(dāng)集的原子語義EX、EG和EU分別給出了驗證算法