CBTC中軌旁安全計算機(jī)的設(shè)計與形式化驗證.pdf

1、隨著計算機(jī)越來越多的應(yīng)用于安全苛求系統(tǒng)中，計算機(jī)能否長期安全、可靠、穩(wěn)定的運行成為人們關(guān)注的中心，這促使著越來越多的人開始研究和設(shè)計安全計算機(jī)。而系統(tǒng)的安全性必須在設(shè)計階段充分考慮，以免由于設(shè)計的缺陷導(dǎo)致整個系統(tǒng)存在安全隱患。所以在系統(tǒng)的設(shè)計過程中，根據(jù)安全苛求系統(tǒng)的“V"型的開發(fā)框架，采用形式化的方法對系統(tǒng)的安全性進(jìn)行建模分析，驗證系統(tǒng)設(shè)計的正確性和完備性是必要的。 論文以基于通信的列車控制(CBTC)系統(tǒng)中ZC應(yīng)用和DSU應(yīng)

2、用作為應(yīng)用背景，以CBTC系統(tǒng)中ZC應(yīng)用和DS應(yīng)用所使用的安全計算機(jī)平臺為例。詳細(xì)分析了安全計算機(jī)平臺需求，在此基礎(chǔ)上確定了系統(tǒng)結(jié)構(gòu)，然后設(shè)計其硬件結(jié)構(gòu)和軟件的調(diào)度策略。 論文引入有色Petri網(wǎng)，根據(jù)安全性設(shè)計思想，在系統(tǒng)的設(shè)計階段對安全計算機(jī)平臺進(jìn)行形式化建模。首先介紹了有色Petri網(wǎng)的形式化層次化建模的方法，然后根據(jù)系統(tǒng)結(jié)構(gòu)，采用“自上而下"的層次建模方法對系統(tǒng)建立的頂層模型和各級子模型，子模型包括“主”“備”通道模型、

3、通道內(nèi)單機(jī)模型、容錯和安全管理單元(FTSM)模型和通信控制器模型。 在所建模型的基礎(chǔ)上，研究了CPN的狀態(tài)空間分析和仿真性能分析兩種方法在模型分析的應(yīng)用。利用狀態(tài)空間分析驗證了容錯和安全管理單元(FTSM)模塊的有界性、活性等動態(tài)行為屬性和邏輯功能的正確性；利用仿真分析完成了系統(tǒng)同步過程的性能分析，得出系統(tǒng)同步的時間參數(shù)，對系統(tǒng)調(diào)度時間的選取具有指導(dǎo)意義。通過對安全計算機(jī)進(jìn)行建模和分析，可以驗證對我們系統(tǒng)設(shè)計是否合理，對系統(tǒng)設(shè)