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

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

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

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