基于可編程邏輯的硬件平臺(tái)的設(shè)計(jì)與形式化驗(yàn)證.pdf

1、安全硬件平臺(tái)通過(guò)先進(jìn)的計(jì)算機(jī)、電子技術(shù)來(lái)現(xiàn)實(shí)。隨著計(jì)算機(jī)、電子技術(shù)的迅猛發(fā)展，系統(tǒng)性能大大提高，結(jié)構(gòu)也變得越來(lái)越復(fù)雜。安全硬件平臺(tái)作為安全苛求系統(tǒng)的重要部分，其安全性是至關(guān)重要的。在設(shè)計(jì)階段就應(yīng)充分考慮安全性，以免由于潛在的設(shè)計(jì)缺陷導(dǎo)致整個(gè)系統(tǒng)存在安全隱患。由于系統(tǒng)逐漸向規(guī)模大、性能強(qiáng)、復(fù)雜性高的方向發(fā)展，單純利用仿真、測(cè)試等方法無(wú)法對(duì)系統(tǒng)進(jìn)行無(wú)窮驗(yàn)證，因此在硬件平臺(tái)設(shè)計(jì)階段，利用形式化方法對(duì)硬件平臺(tái)設(shè)計(jì)的正確性和完備性進(jìn)行驗(yàn)證。

2、 論文以基于通信的列車控制（Communication-based Train Control，CBTC）系統(tǒng)為應(yīng)用背景，詳細(xì)分析了安全硬件平臺(tái)需求。通過(guò)對(duì)比各種平臺(tái)結(jié)構(gòu)的優(yōu)缺點(diǎn)，選取了二乘二取二結(jié)構(gòu)為本文設(shè)計(jì)的總體結(jié)構(gòu)。在分析各種安全計(jì)算機(jī)結(jié)構(gòu)的基礎(chǔ)上，結(jié)合CBTC系統(tǒng)對(duì)安全硬件平臺(tái)的功能需求，提出一種新的二取二系統(tǒng)結(jié)構(gòu)方案。 論文設(shè)計(jì)的安全硬件平臺(tái)是以安全性、通用性為重點(diǎn)。論文詳細(xì)介紹了保證安全性、通用性和調(diào)度策略的具體功

3、能實(shí)現(xiàn)方法。以微同步和硬件數(shù)據(jù)比較方式來(lái)保證平臺(tái)的安全性；以處理器的約束、數(shù)據(jù)幀結(jié)構(gòu)的確定和接口格式的固定來(lái)保證了平臺(tái)的通用性。 安全硬件平臺(tái)中的重要單元是安全比較核。安全比較核基于可編程邏輯設(shè)計(jì)與實(shí)現(xiàn)。使用可編程邏輯不僅可以縮減電路的體積，提高電路的穩(wěn)定性，而且先進(jìn)的開(kāi)發(fā)工具使整個(gè)系統(tǒng)的設(shè)計(jì)調(diào)試周期大大縮短。在實(shí)現(xiàn)過(guò)程中，將安全比較核劃分為不同的功能子模塊，對(duì)每個(gè)子模塊進(jìn)行設(shè)計(jì)與實(shí)現(xiàn)，并且對(duì)仿真結(jié)果進(jìn)行分析，保證其設(shè)計(jì)基本正確

4、。 仿真驗(yàn)證只能保證比較核的仿真結(jié)果正確，但對(duì)于復(fù)雜系統(tǒng)，無(wú)窮盡的仿真是不現(xiàn)實(shí)的。為了避免存在潛在的設(shè)計(jì)錯(cuò)誤，論文利用基于斷言的方法（Property Specification Language，PSL）對(duì)安全比較核進(jìn)行形式化驗(yàn)證，對(duì)其內(nèi)部設(shè)計(jì)的正確性和完整性進(jìn)行檢驗(yàn)。當(dāng)斷言失敗，發(fā)現(xiàn)設(shè)計(jì)錯(cuò)誤時(shí)，對(duì)檢驗(yàn)出的設(shè)計(jì)錯(cuò)誤進(jìn)行分析、修改。再進(jìn)行新的驗(yàn)證，直到形式化驗(yàn)證證明其設(shè)計(jì)沒(méi)有潛在的設(shè)計(jì)缺陷為止。 論文結(jié)果表明，對(duì)于基于可