面向混成特性的CTCS-3系統(tǒng)規(guī)劃建模與驗證.pdf

1、系統(tǒng)規(guī)范是系統(tǒng)開發(fā)的起點和基礎(chǔ)。系統(tǒng)規(guī)范的缺陷將給項目成功帶來極大的風(fēng)險。對系統(tǒng)規(guī)范進(jìn)行建模和驗證是消除潛在缺陷的有效方法，也是保證系統(tǒng)正確設(shè)計和開發(fā)的前提。
　　近些年來，中國軌道交通事業(yè)快速發(fā)展。以CTCS-3級列車運行控制系統(tǒng)為代表的基于無線通信的列車運行控制系統(tǒng)是今后的發(fā)展方向。CTCS-3級列車運行控制系統(tǒng)系統(tǒng)是一個典型的混成系統(tǒng)，列車的連續(xù)運行過程和無線閉塞中心(RBC)的離散作用機制之間交互影響，呈現(xiàn)復(fù)雜的混成性。列

2、車事故的發(fā)生往往同速度、加速度、距離等連續(xù)變化量的不良控制密切相關(guān)。因此，從混成性的角度對安全關(guān)鍵CTCS-3系統(tǒng)規(guī)范進(jìn)行建模與驗證是非常有必要和有意義的。
　　以此為出發(fā)點，本文在列車運行控制系統(tǒng)規(guī)范建模與驗證體系的基礎(chǔ)上，給出面向混成性的CTCS-3系統(tǒng)規(guī)范建模與驗證的方法和流程：首先利用可描述系統(tǒng)混成性的HybridUML對CTCS-3系統(tǒng)規(guī)范建模，接著將模型轉(zhuǎn)換為形式化的微分動態(tài)邏輯模型，最后在驗證工具里對系統(tǒng)規(guī)范的微分動

3、態(tài)邏輯模型進(jìn)行形式化驗證。
　　本文重點闡述了基于UML2.0的擴展機制在建模軟件RSA中構(gòu)建概要文件(profile)實現(xiàn)UML2.0到HybridUML擴展的過程；同時以列車運動加速減速過程為例闡述了如何利用經(jīng)擴展得到的HybridUML對CTCS-3系統(tǒng)規(guī)范進(jìn)行建模；接著給出了從HybridUML模型到微分動態(tài)邏輯模型的轉(zhuǎn)換規(guī)則，進(jìn)而使CTCS-3系統(tǒng)的形式化模型的獲得和對模型的形式化驗證能夠得以實現(xiàn)。
　　最后本文以

4、CTCS-3系統(tǒng)中典型的RBC切換流程為案例，給出了面向混成性的CTCS-3系統(tǒng)規(guī)范建模與驗證的方法的具體應(yīng)用。首先介紹了CTCS-3系統(tǒng)規(guī)范中RBC切換流程的過程，接著在RSA中對RBC切換流程建立HybridUML模型，然后根據(jù)從HybridUML到微分動態(tài)邏輯的轉(zhuǎn)換規(guī)則得到RBC切換的微分動態(tài)邏輯模型，最后在形式化驗證工具KeYmaera中對微分動態(tài)邏輯模型的安全性等性質(zhì)進(jìn)行驗證并對驗證結(jié)果進(jìn)行了分析。案例分析很好地展示了面向混成