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

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

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

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