基于虛擬化的列控安全計算機平臺分區(qū)軟件研究.pdf

1、隨著我國高速鐵路和城市軌道交通快速發(fā)展，列車運行控制系統(tǒng)（列控系統(tǒng)）功能需求日益復(fù)雜化，如高密度行車控制、節(jié)能優(yōu)化、以及無人駕駛等。列控安全計算機作為列控系統(tǒng)應(yīng)用的重要載體，其平臺上實時軟件也越加復(fù)雜化。本文針對列控安全計算機軟件復(fù)雜化和系統(tǒng)需求不斷地變化等趨勢，提出了一種基于虛擬化的多應(yīng)用列控安全計算機平臺分區(qū)軟件設(shè)計方法。
　　首先分析了列控安全計算機平臺特性以及國內(nèi)外軟件安全標(biāo)準(zhǔn)需求，確定了在復(fù)雜系統(tǒng)中模塊化抽象化設(shè)計思路和

2、相關(guān)安全軟件內(nèi)核技術(shù)。根據(jù)安全需求研究基于虛擬化技術(shù)的分區(qū)軟件技術(shù)理論以及其應(yīng)用，表明分區(qū)軟件適用于解決列控安全計算機平臺所面臨的軟件復(fù)雜化問題。同時也論證了分區(qū)軟件系統(tǒng)的并發(fā)性和共享性特征給系統(tǒng)帶來的安全性風(fēng)險，進(jìn)而分析幾種典型的并發(fā)系統(tǒng)安全性控制算法，并針對性地提出了基于并發(fā)分離邏輯的形式化驗證方法。
　　接著，根據(jù)容錯性、實時性、分層化的設(shè)計需求分別從時間和空間隔離機制、并發(fā)控制策略、分區(qū)間通信機制、實時容錯調(diào)度算法四個方面

3、進(jìn)行詳細(xì)設(shè)計。第一，根據(jù)故障隔離設(shè)計目標(biāo)，分別提出了基于內(nèi)存管理單元(MMU)的空間隔離方法和基于強制時間調(diào)度的時間隔離模型，以滿足系統(tǒng)故障隔離要求;第二，對于并發(fā)系統(tǒng)安全性問題，設(shè)計了基于事務(wù)內(nèi)存的并發(fā)安全控制機制，并利用并發(fā)分離邏輯和不變式證明方法對于該機制進(jìn)行形式化驗證，證明結(jié)果表明了該機制能保護(hù)并發(fā)程序的正確性;第三，在分區(qū)間通信機制方面，根據(jù)分區(qū)間通信的實時性和可靠性需求，設(shè)計了基于客戶/服務(wù)端(C/S)模型的實時通信機制;第