模型驅(qū)動的城軌列車車載控制系統(tǒng)軟件評估體系.pdf

1、在城軌列車運行車載控制系統(tǒng)中，硬件和軟件同等重要，車載硬件已經(jīng)逐步采用標(biāo)準(zhǔn)工業(yè)計算機產(chǎn)品，而負(fù)責(zé)實現(xiàn)核心功能的軟件，已經(jīng)成為保障列車安全高效運營的一個重要因素。由軟件錯誤導(dǎo)致事故發(fā)生將會造成生命財產(chǎn)重大損失，所以針對城軌車載軟件開發(fā)前期過程中的模型建立，模型測試、模型驗證方法的研究具有重要意義。列控系統(tǒng)軟件是多層次結(jié)構(gòu)的復(fù)雜系統(tǒng)，具有并發(fā)性、響應(yīng)性特性和狀態(tài)空間龐大的特點，研究適合描述軟件需求的基于模型驅(qū)動的建模方法、模型狀態(tài)的轉(zhuǎn)換、相

2、關(guān)測試序列生成驗證方法和模型軟件測試，全套流程已經(jīng)成為城軌列控系統(tǒng)軟件的系統(tǒng)級建模評估理論的研究重點。
　　根據(jù)城軌列控系統(tǒng)軟件的需求及其實際功能相關(guān)的特點，提出了針對軟件的建模技術(shù)、序列生成驗證及測試方法。
　　建模方面，從城軌列控軟件需求出發(fā)，提出了基于模型驅(qū)動的軟件架構(gòu)的需求分析和功能劃分，以車載設(shè)備軟件為應(yīng)用對象，使用了標(biāo)準(zhǔn)化建模語言UML，以圖形化方式表述軟件系統(tǒng)過程和實現(xiàn)方法。分析了具體模型的分層架構(gòu)，用兩種靜態(tài)

3、圖和兩種動態(tài)圖從不同層面對細節(jié)進行了描述，對內(nèi)建關(guān)聯(lián)進行了層次連接。
　　驗證方面，介紹了模型檢驗的概念，說明了計算樹邏輯(CTL)的擴展形式ASK-CTL在著色Petri網(wǎng)上的應(yīng)用。從圖的遍歷角度，提出了深度優(yōu)先算法在尋找有效測試路徑的概念，并將算法運用于CPN Tools，以生成測試案例路徑。引入實際的列控系統(tǒng)模型，提出了一種針對多線程的形式化定義ThrCPN及其圖形描述，和基于對象UML模型的形式化建模方法ObjCPN。在層

4、次化建模方法中，分別運用了ThrCPN和ObjCPN。提出了UML模型轉(zhuǎn)換形式化有色Petri網(wǎng)的轉(zhuǎn)換方法，縮小了功能模型到驗證方案之間差距，簡化了轉(zhuǎn)換的復(fù)雜過程，形成了可驗證的形式化模型。
　　測試序列生成方面，在CPN Tools工具中應(yīng)用了ML編寫的深度優(yōu)先搜索算法，生成的測試序列，解決了并發(fā)系統(tǒng)不可達狀態(tài)過多的問題。形式化驗證方法生成的案例工具為形式化檢驗的主要于段。測試序列的生成對后期軟件模擬測試起到了測試案例的作用。對