列控系統(tǒng)混成行為的建模與驗證方法.pdf

1、隨著列控技術(shù)的發(fā)展，列車運行控制系統(tǒng)獲得了巨大的進步和發(fā)展。在系統(tǒng)的設(shè)計和開發(fā)階段，為了確保列控系統(tǒng)的安全性，列控系統(tǒng)需求規(guī)范的正確性起著越來越重要的作用。然而，在系統(tǒng)開發(fā)的初始階段，通常會因為系統(tǒng)需求規(guī)范不完整而無法進行開發(fā)。在這種情況下，如何確定系統(tǒng)的關(guān)鍵參數(shù)成為主要的研究課題。同時，現(xiàn)有研究成果表明，在需求層面，分析和驗證系統(tǒng)模型中的關(guān)鍵參數(shù)面臨很多困難。因此，為了解決系統(tǒng)模型中關(guān)鍵參數(shù)的分析問題，需要提出一種合理的系統(tǒng)屬性建模和

2、形式化驗證的框架結(jié)構(gòu)。
　　列控系統(tǒng)需求規(guī)范的分析過程包括兩部的內(nèi)容，建立系統(tǒng)規(guī)范模型和對該形式化模型進行驗證。一方面，統(tǒng)一建模語言(UML)是一種面向?qū)ο蟮慕ＵZ言，已廣泛應(yīng)用于不同工程領(lǐng)域。然而，列控系統(tǒng)屬于典型的混成系統(tǒng)和安全苛求系統(tǒng)。正確地刻畫系統(tǒng)的混成特性給列控系統(tǒng)需求規(guī)范的建模工作帶來了巨大的挑戰(zhàn)。另一方面，形式化方法已成為保障安全苛求系統(tǒng)的安全性與可靠性的重要手段。根據(jù)不同的分析或驗證要求，設(shè)計者可以選擇不同的形式化

3、驗證工具進行相關(guān)的驗證工作。
　　因此，本文從列控系統(tǒng)需求規(guī)范建模方法與驗證工具集成著手進行研究，主要內(nèi)容包括:
　　1.對列控系統(tǒng)混成特性進行分析，研究UML擴展機制，設(shè)計混成UML概要文件，使之能夠準確地刻畫列控系統(tǒng)的混成特性。
　　2.為了驗證混成系統(tǒng)的安全性，提出了時間有界的可達性分析算法。該算法基于BMC驗證技術(shù)，對具體的自動機模型運用該算法可以計算有界時間內(nèi)系統(tǒng)的所有可執(zhí)行路徑。時間有界的可達性分析算法適用

4、于線性或非線性混成自動機的驗證。
　　3.以移動閉塞中的追蹤模型為案例，運用提出的混成UML概要文件對其進行建模;并根據(jù)轉(zhuǎn)換規(guī)則將所建的列車追蹤擴展模型轉(zhuǎn)換為HYTECH模型;在開發(fā)的驗證支持工具中完成了該模型的驗證分析工作。通過案例分析，證明所提出的基于UML擴展機制對列控系統(tǒng)混成行為建模方法的可行性，以及所開發(fā)驗證支持工具的可用性。
　　4.在Topcased平臺上完成了驗證工具的軟件開發(fā)。Topcased平臺上集成了U