【摘要】： 安全硬件平臺通過先進的計算機、電子技術(shù)來現(xiàn)實。隨著計算機、電子技術(shù)的迅猛發(fā)展,系統(tǒng)性能大大提高,結(jié)構(gòu)也變得越來越復雜。安全硬件平臺作為安全苛求系統(tǒng)的重要部分,其安全性是至關(guān)重要的。在設(shè)計階段就應(yīng)充分考慮安全性,以免由于潛在的設(shè)計缺陷導致整個系統(tǒng)存在安全隱患。由于系統(tǒng)逐漸向規(guī)模大、性能強、復雜性高的方向發(fā)展,單純利用仿真、測試等方法無法對系統(tǒng)進行無窮驗證,因此在硬件平臺設(shè)計階段,利用形式化方法對硬件平臺設(shè)計的正確性和完備性進行驗證。 論文以基于通信的列車控制(Communication-based Train Control,CBTC)系統(tǒng)為應(yīng)用背景,詳細分析了安全硬件平臺需求。通過對比各種平臺結(jié)構(gòu)的優(yōu)缺點,選取了二乘二取二結(jié)構(gòu)為本文設(shè)計的總體結(jié)構(gòu)。在分析各種安全計算機結(jié)構(gòu)的基礎(chǔ)上,結(jié)合CBTC系統(tǒng)對安全硬件平臺的功能需求,提出一種新的二取二系統(tǒng)結(jié)構(gòu)方案。 論文設(shè)計的安全硬件平臺是以安全性、通用性為重點。論文詳細介紹了保證安全性、通用性和調(diào)度策略的具體功能實現(xiàn)方法。以微同步和硬件數(shù)據(jù)比較方式來保證平臺的安全性;以處理器的約束、數(shù)據(jù)幀結(jié)構(gòu)的確定和接口格式的固定來保證了平臺的通用性。 安全硬件平臺中的重要單元是安全比較核。安全比較核基于可編程邏輯設(shè)計與實現(xiàn)。使用可編程邏輯不僅可以縮減電路的體積,提高電路的穩(wěn)定性,而且先進的開發(fā)工具使整個系統(tǒng)的設(shè)計調(diào)試周期大大縮短。在實現(xiàn)過程中,將安全比較核劃分為不同的功能子模塊,對每個子模塊進行設(shè)計與實現(xiàn),并且對仿真結(jié)果進行分析,保證其設(shè)計基本正確。 仿真驗證只能保證比較核的仿真結(jié)果正確,但對于復雜系統(tǒng),無窮盡的仿真是不現(xiàn)實的。為了避免存在潛在的設(shè)計錯誤,論文利用基于斷言的方法(PropertySpecification Language,PSL)對安全比較核進行形式化驗證,對其內(nèi)部設(shè)計的正確性和完整性進行檢驗。當斷言失敗,發(fā)現(xiàn)設(shè)計錯誤時,對檢驗出的設(shè)計錯誤進行分析、修改。再進行新的驗證,直到形式化驗證證明其設(shè)計沒有潛在的設(shè)計缺陷為止。 論文結(jié)果表明,對于基于可編程邏輯設(shè)計的安全硬件平臺,利用斷言對設(shè)計進行形式化驗證,可以檢驗出仿真無法檢驗出的錯誤,保證其設(shè)計的完整性和正確性,從而得到一個無設(shè)計缺陷、通用的安全硬件平臺。
【學位授予單位】：北京交通大學
【學位級別】：碩士
【學位授予年份】：2009
【分類號】：TP302
【圖文】：

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

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

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

【引證文獻】

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

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

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

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

本文編號：2761472