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

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

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

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