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

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

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

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

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