

版權說明:本文檔由用戶提供并上傳,收益歸屬內容提供方,若內容存在侵權,請進行舉報或認領
文檔簡介
1、安全硬件平臺通過先進的計算機、電子技術來現(xiàn)實。隨著計算機、電子技術的迅猛發(fā)展,系統(tǒng)性能大大提高,結構也變得越來越復雜。安全硬件平臺作為安全苛求系統(tǒng)的重要部分,其安全性是至關重要的。在設計階段就應充分考慮安全性,以免由于潛在的設計缺陷導致整個系統(tǒng)存在安全隱患。由于系統(tǒng)逐漸向規(guī)模大、性能強、復雜性高的方向發(fā)展,單純利用仿真、測試等方法無法對系統(tǒng)進行無窮驗證,因此在硬件平臺設計階段,利用形式化方法對硬件平臺設計的正確性和完備性進行驗證。
2、 論文以基于通信的列車控制(Communication-based Train Control,CBTC)系統(tǒng)為應用背景,詳細分析了安全硬件平臺需求。通過對比各種平臺結構的優(yōu)缺點,選取了二乘二取二結構為本文設計的總體結構。在分析各種安全計算機結構的基礎上,結合CBTC系統(tǒng)對安全硬件平臺的功能需求,提出一種新的二取二系統(tǒng)結構方案。 論文設計的安全硬件平臺是以安全性、通用性為重點。論文詳細介紹了保證安全性、通用性和調度策略的具體功
3、能實現(xiàn)方法。以微同步和硬件數(shù)據比較方式來保證平臺的安全性;以處理器的約束、數(shù)據幀結構的確定和接口格式的固定來保證了平臺的通用性。 安全硬件平臺中的重要單元是安全比較核。安全比較核基于可編程邏輯設計與實現(xiàn)。使用可編程邏輯不僅可以縮減電路的體積,提高電路的穩(wěn)定性,而且先進的開發(fā)工具使整個系統(tǒng)的設計調試周期大大縮短。在實現(xiàn)過程中,將安全比較核劃分為不同的功能子模塊,對每個子模塊進行設計與實現(xiàn),并且對仿真結果進行分析,保證其設計基本正確
4、。 仿真驗證只能保證比較核的仿真結果正確,但對于復雜系統(tǒng),無窮盡的仿真是不現(xiàn)實的。為了避免存在潛在的設計錯誤,論文利用基于斷言的方法(Property Specification Language,PSL)對安全比較核進行形式化驗證,對其內部設計的正確性和完整性進行檢驗。當斷言失敗,發(fā)現(xiàn)設計錯誤時,對檢驗出的設計錯誤進行分析、修改。再進行新的驗證,直到形式化驗證證明其設計沒有潛在的設計缺陷為止。 論文結果表明,對于基于可
溫馨提示
- 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
- 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權益歸上傳用戶所有。
- 3. 本站RAR壓縮包中若帶圖紙,網頁內容里面會有圖紙預覽,若沒有圖紙預覽就沒有圖紙。
- 4. 未經權益所有人同意不得將文件中的內容挪作商業(yè)或盈利用途。
- 5. 眾賞文庫僅提供信息存儲空間,僅對用戶上傳內容的表現(xiàn)方式做保護處理,對用戶上傳分享的文檔內容本身不做任何修改或編輯,并不能對任何下載內容負責。
- 6. 下載文件中如有侵權或不適當內容,請與我們聯(lián)系,我們立即糾正。
- 7. 本站不保證下載資源的準確性、安全性和完整性, 同時也不承擔用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。
最新文檔
- 基于高階邏輯系統(tǒng)HOL的數(shù)字硬件形式化驗證.pdf
- 可編程邏輯器件的可測性設計與驗證平臺的搭建.pdf
- 混合系統(tǒng)的形式化驗證.pdf
- 可編程邏輯器件結構庫的生成與驗證.pdf
- 基于NuSMV的AUML模型形式化驗證.pdf
- 可信信道協(xié)議的設計與形式化驗證.pdf
- 基于VHDL的可編程邏輯器件虛擬實驗平臺的設計與實現(xiàn).pdf
- 基于圖論的形式化驗證方法的研究與實現(xiàn).pdf
- 基于可編程硬件的骨骼蒙皮動畫的設計與實現(xiàn).pdf
- 基于模型檢測的SET協(xié)議形式化驗證與改進.pdf
- 基于開放時態(tài)邏輯的面向方面程序形式化驗證和模塊推理研究.pdf
- 高性能DSP可編程邏輯控制平臺的研究.pdf
- 基于模型檢測的UML形式化驗證的研究.pdf
- 自動導引車的建模與形式化驗證.pdf
- 安全協(xié)議形式化驗證方法的研究.pdf
- FPGA中可編程邏輯單元的設計與研究.pdf
- 可編程邏輯器件設計技巧
- 動態(tài)可重構系統(tǒng)形式化驗證工具與原型平臺的設計與實現(xiàn).pdf
- 帶參協(xié)議形式化驗證的研究.pdf
- 基于可編程邏輯原理的微機保護實驗裝置設計.pdf
評論
0/150
提交評論