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

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

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

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

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