【摘要】： 安全硬件平臺(tái)通過先進(jìn)的計(jì)算機(jī)、電子技術(shù)來現(xiàn)實(shí)。隨著計(jì)算機(jī)、電子技術(shù)的迅猛發(fā)展,系統(tǒng)性能大大提高,結(jié)構(gòu)也變得越來越復(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è)試等方法無法對(duì)系統(tǒng)進(jìn)行無窮驗(yàn)證,因此在硬件平臺(tái)設(shè)計(jì)階段,利用形式化方法對(duì)硬件平臺(tái)設(shè)計(jì)的正確性和完備性進(jìn)行驗(yàn)證。 論文以基于通信的列車控制(Communication-based Train Control,CBTC)系統(tǒng)為應(yīng)用背景,詳細(xì)分析了安全硬件平臺(tái)需求。通過對(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)度策略的具體功能實(shí)現(xiàn)方法。以微同步和硬件數(shù)據(jù)比較方式來保證平臺(tái)的安全性;以處理器的約束、數(shù)據(jù)幀結(jié)構(gòu)的確定和接口格式的固定來保證了平臺(tái)的通用性。 安全硬件平臺(tái)中的重要單元是安全比較核。安全比較核基于可編程邏輯設(shè)計(jì)與實(shí)現(xiàn)。使用可編程邏輯不僅可以縮減電路的體積,提高電路的穩(wěn)定性,而且先進(jìn)的開發(fā)工具使整個(gè)系統(tǒng)的設(shè)計(jì)調(diào)試周期大大縮短。在實(shí)現(xiàn)過程中,將安全比較核劃分為不同的功能子模塊,對(duì)每個(gè)子模塊進(jìn)行設(shè)計(jì)與實(shí)現(xiàn),并且對(duì)仿真結(jié)果進(jìn)行分析,保證其設(shè)計(jì)基本正確。 仿真驗(yàn)證只能保證比較核的仿真結(jié)果正確,但對(duì)于復(fù)雜系統(tǒng),無窮盡的仿真是不現(xiàn)實(shí)的。為了避免存在潛在的設(shè)計(jì)錯(cuò)誤,論文利用基于斷言的方法(PropertySpecification 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ì)沒有潛在的設(shè)計(jì)缺陷為止。 論文結(jié)果表明,對(duì)于基于可編程邏輯設(shè)計(jì)的安全硬件平臺(tái),利用斷言對(duì)設(shè)計(jì)進(jìn)行形式化驗(yàn)證,可以檢驗(yàn)出仿真無法檢驗(yàn)出的錯(cuò)誤,保證其設(shè)計(jì)的完整性和正確性,從而得到一個(gè)無設(shè)計(jì)缺陷、通用的安全硬件平臺(tái)。
【學(xué)位授予單位】：北京交通大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2009
【分類號(hào)】：TP302
【圖文】：

機(jī)仍會(huì)繼續(xù)運(yùn)行下去，如果到下一個(gè)同步點(diǎn)仍然失步，且在連續(xù)的五次同步中失步三次，則表示雙機(jī)完全失步，通過安全比較核對(duì)系統(tǒng)進(jìn)行失步處理。同步處理過程如圖3一2所示。同步開始\\N}司步1-卜二一同步2，)卜同步3同步2卜同步3同步4N同步3沐卜同步4同步5\)失步失步失步Y(jié)Y一丫下一v-}暨i」一同步…圖3一2同步處理過程Fig.3一25 擔(dān)chronizationexecutiveProeess從安全性和可用性的角度分析，這種方法在任務(wù)同步的基礎(chǔ)上添加了時(shí)間片檢測(cè)點(diǎn)同步，提高了系統(tǒng)的安全性，彌補(bǔ)了反應(yīng)時(shí)間不足的缺點(diǎn)，同時(shí)也容忍了瞬時(shí)故障所造成的失步，使系統(tǒng)的可用性大大提高。任務(wù)同步檢測(cè)點(diǎn)由處理器內(nèi)部程序控制，時(shí)間片同步檢測(cè)點(diǎn)由外部安全比較核控制，處理器和比較核各自記錄同步歷史數(shù)據(jù)，這樣可以防止一方出現(xiàn)故障所導(dǎo)致的系統(tǒng)同步故障，或者出現(xiàn)同步檢測(cè)故障，使系統(tǒng)出現(xiàn)危險(xiǎn)輸出。3.1.2安全硬件平臺(tái)數(shù)據(jù)比較方式數(shù)據(jù)比較是二取二系統(tǒng)中保證安全的重要措施

匕京交通大學(xué)碩十學(xué)位論種可編程電路是:可編程邏輯塊 (ConfigurableLogicBlock，cLB)、輸入/輸出模塊(I/oBloek，IoB)和互連資源(IntereoimectResource，IR)，其基本的結(jié)構(gòu)圖如圖4一l所示。墉 墉墉…烈 烈洲 洲 … …口 口… … 一一一一一一一一一一一一一一一一一一一一一一一一一一一一一;蒙 -----------------------------------------------------黛黛篡黔 黔 黔一卡斗一 一油睡 睡‘一羹翻禽入從獷 ---一斗一十一 一 一嚼冷 冷立 立立立立姍扛 扛 扛__二:轟 ___~-‘氦一 一一一一 甲舞哪哪 哪全 全 全 全 全 全全徹讓 讓 讓。一;才、 、犯 犯 犯 犯犯犯犯犯犯 犯犯犯 犯 犯 犯犯犯犯犯犯犯 犯 犯 犯

PSL結(jié)構(gòu)

【引證文獻(xiàn)】

相關(guān)期刊論文 前1條

1 劉明端;穆建成;馬連川;尚麟宇;;基于模型的安全比較核設(shè)計(jì)[J];沈陽建筑大學(xué)學(xué)報(bào)(自然科學(xué)版);2011年04期

相關(guān)碩士學(xué)位論文 前1條

1 劉海旭;ARINC 659通信總線的設(shè)計(jì)與實(shí)現(xiàn)[D];北京交通大學(xué);2010年

本文編號(hào)：2761472