列控安全計(jì)算機(jī)平臺(tái)測(cè)試方法研究.pdf

1、與區(qū)域控制器和數(shù)據(jù)存儲(chǔ)單元有著密切交互的安全計(jì)算機(jī)平臺(tái)是列控系統(tǒng)中的核心裝備和重要安全單元之一。為了打破技術(shù)封鎖，擁有自主化安全計(jì)算機(jī)平臺(tái)，北京交通大學(xué)軌道交通控制與安全國(guó)家重點(diǎn)實(shí)驗(yàn)室已經(jīng)開(kāi)發(fā)出下一代列控安全計(jì)算機(jī)平臺(tái)。為了滿足下一代安全計(jì)算機(jī)平臺(tái)測(cè)試的需要，本文對(duì)安全計(jì)算機(jī)平臺(tái)測(cè)試方法進(jìn)行了研究。在調(diào)查研究一般安全苛求系統(tǒng)和以往安全計(jì)算機(jī)平臺(tái)測(cè)試文獻(xiàn)的基礎(chǔ)上，針對(duì)其中各測(cè)試階段采用不同測(cè)試方法無(wú)法滿足測(cè)試方法普遍性和不做需求追蹤工作或

2、將需求追蹤、測(cè)試分開(kāi)無(wú)法實(shí)現(xiàn)統(tǒng)一性的問(wèn)題，本文提出一種通用的安全苛求系統(tǒng)混合測(cè)試方法，并將其應(yīng)用到安全計(jì)算機(jī)平臺(tái)測(cè)試當(dāng)中。
　　首先，本文設(shè)計(jì)了混合測(cè)試方法的技術(shù)方案，并對(duì)其中提取系統(tǒng)需求、構(gòu)建系統(tǒng)可追綜性信息流、模型轉(zhuǎn)換和解析、測(cè)試序列自動(dòng)生成、測(cè)試結(jié)果結(jié)構(gòu)和需求覆蓋分析5項(xiàng)主要技術(shù)方法的現(xiàn)狀和實(shí)現(xiàn)過(guò)程做了分析和介紹。
　　其次，將混合測(cè)試方法運(yùn)用到安全計(jì)算機(jī)平臺(tái)測(cè)試之中。從測(cè)試模型和系統(tǒng)工作模式狀態(tài)兩個(gè)方面分解出安全計(jì)算

3、機(jī)平臺(tái)系統(tǒng)級(jí)、子系統(tǒng)集成級(jí)和單元模塊級(jí)的功能特征組，在此基礎(chǔ)上提取出安全計(jì)算機(jī)平臺(tái)需求列表。構(gòu)建了安全計(jì)算機(jī)平臺(tái)可追綜性信息流:用rational rose畫出安全計(jì)算機(jī)平臺(tái)用例圖，編制了用例圖轉(zhuǎn)類圖和類圖轉(zhuǎn)狀態(tài)圖的轉(zhuǎn)換規(guī)則，得到了安全計(jì)算機(jī)平臺(tái)類圖和狀態(tài)圖，提取了安全計(jì)算機(jī)平臺(tái)的需求關(guān)鍵字，編制了安全計(jì)算機(jī)平臺(tái)需求數(shù)據(jù)結(jié)構(gòu)，通過(guò)改進(jìn)SHA-1算法得到需求哈希值，作為需求的指紋識(shí)別用于后續(xù)需求追蹤。
　　構(gòu)建UML類圖、狀態(tài)圖元模

4、型和NuSMV元模型，從元模型的角度分析和編制了UML模型與NuSMV模型的轉(zhuǎn)換規(guī)則，采用KM3語(yǔ)言編寫了元模型，采用ATL語(yǔ)言編寫了轉(zhuǎn)換程序，在Eclipse環(huán)境的ATL平臺(tái)下采用ATL轉(zhuǎn)換框架將安全計(jì)算機(jī)平臺(tái)狀態(tài)圖轉(zhuǎn)換為NuSMV模型并解析得到SMV程序;在SMV程序SPEC模塊下添加用CTL描述滿足MC/DC測(cè)試覆蓋標(biāo)準(zhǔn)的安全計(jì)算機(jī)平臺(tái)性質(zhì)，采用NuSMV模型驗(yàn)證器得到平臺(tái)測(cè)試序列。
　　最后，搭建了安全計(jì)算機(jī)平臺(tái)測(cè)試系統(tǒng)，