應(yīng)答器報文編制規(guī)則的建模、驗證與應(yīng)用.pdf

1、應(yīng)答器系統(tǒng)作為實現(xiàn)地-車信息傳輸?shù)闹匾O(shè)備，其向車載傳輸?shù)膱笪臄?shù)據(jù)的正確性直接關(guān)系到列車運行安全。應(yīng)答器報文是由編制人員依據(jù)應(yīng)答器應(yīng)用原則將線路工程數(shù)據(jù)進行編制而得。然而應(yīng)用原則只是從列控系統(tǒng)功能需求的角度定義了應(yīng)答器的設(shè)置原則以及報文結(jié)構(gòu)，并未具體描述如何編制報文;此外，基于文本語言描述的應(yīng)用原則易產(chǎn)生二義性問題，簡單地將應(yīng)用原則轉(zhuǎn)換為相關(guān)軟件代碼存在很大隱患。
　　本論文針對上述問題，首先基于應(yīng)用原則的要求，結(jié)合專家經(jīng)驗，提取

2、出一套具體完備的報文編制規(guī)則，之后，針對編制規(guī)則的特點，提出一種對其建模驗證的方法框架，其主要特點是能夠在編制規(guī)則、模型、驗證過程以及模型檢驗結(jié)果之間建立一條雙向跟蹤鏈。通過分析模型檢驗結(jié)果，不斷迭代規(guī)則模型，最終得到滿足質(zhì)量要求的報文編制規(guī)則及對應(yīng)模型，可用于指導(dǎo)報文編制以及相關(guān)工具的開發(fā)，這對確保報文數(shù)據(jù)的正確性有重要意義，且為后續(xù)應(yīng)答器報文相關(guān)技術(shù)規(guī)范的修訂提供支持。
　　本文基于以上述過程，具體做了以下三個方面的工作:

3、r>　　(1)從數(shù)據(jù)生命周期和數(shù)據(jù)結(jié)構(gòu)的角度分析了應(yīng)答器報文數(shù)據(jù)，總結(jié)了報文數(shù)據(jù)從生成、使用、歸檔到過時的全過程;構(gòu)建了工程數(shù)據(jù)和報文數(shù)據(jù)的結(jié)構(gòu)模型。之后深入挖掘分析應(yīng)答器應(yīng)用原則的內(nèi)容要求，并總結(jié)分析了相關(guān)的專家經(jīng)驗，作為后續(xù)編制規(guī)則建模驗證的基礎(chǔ)。
　　(2)以應(yīng)答器應(yīng)用原則等相關(guān)規(guī)范文檔和專家經(jīng)驗為輸入，提取出報文編制規(guī)則的整體框架，以具體類型的應(yīng)答器對應(yīng)的報文生成場景為例，對編制規(guī)則進行建模驗證。首先對規(guī)則進行非形式化分析

4、，輸出規(guī)則管理報表以實現(xiàn)規(guī)則到模型的正向追蹤;采用基于UML-NuSMV相結(jié)合的建模驗證方法，建立報文編制規(guī)則的UML模型，之后將其用NuSMV形式化語言描述，輸入模型檢驗工具進行驗證，分析驗證結(jié)果，不斷修改、重新驗證反例中的錯誤直至驗證結(jié)果全部為真，最終得到滿足質(zhì)量要求的編制規(guī)則及對應(yīng)模型。
　　(3)基于編制規(guī)則和對應(yīng)模型，開發(fā)自動化報文編制工具。以已開通的實際線路數(shù)據(jù)為例編制應(yīng)答器報文，將工具生成的報文與線上使用的正確報文數(shù)