列控系統(tǒng)需求規(guī)范形式化建模與驗(yàn)證方法研究.pdf

1、列車運(yùn)行控制系統(tǒng)（以下簡(jiǎn)稱“列控系統(tǒng)”）需求規(guī)范是列控系統(tǒng)設(shè)計(jì)與開發(fā)的基礎(chǔ)，是實(shí)現(xiàn)互聯(lián)互通以及確保系統(tǒng)高效率與安全性的關(guān)鍵環(huán)節(jié)。然而，由于列控系統(tǒng)是一個(gè)復(fù)雜的安全苛求系統(tǒng)，僅依靠經(jīng)驗(yàn)制定的系統(tǒng)需求規(guī)范不可避免地存在某些漏洞或者安全隱患。另外，用自然語言刻畫的系統(tǒng)需求規(guī)范可能存在歧義，這為系統(tǒng)的設(shè)計(jì)與開發(fā)帶來不利影響。因此對(duì)列控系統(tǒng)需求規(guī)范進(jìn)行形式化建模與驗(yàn)證顯得十分必要。
　　本文以我國(guó)CTCS-3級(jí)列控系統(tǒng)需求規(guī)范為應(yīng)用背景，圍

2、繞系統(tǒng)需求規(guī)范的建模與驗(yàn)證方法展開研究。首先，提出了一種改進(jìn)型列控系統(tǒng)需求規(guī)范形式化建模與驗(yàn)證方法，其主要特點(diǎn)是能夠在系統(tǒng)需求規(guī)范、模型、驗(yàn)證過程以及驗(yàn)證結(jié)果之間建立一條雙向、完整的追蹤鏈，始終保證系統(tǒng)需求規(guī)范、模型以及程序代碼之間的一致性。然后，在該方法的基礎(chǔ)上，對(duì)如何保證模型與系統(tǒng)需求規(guī)范的一致性和覆蓋性，以及系統(tǒng)需求規(guī)范的UML模型與CSP模型之間的轉(zhuǎn)換技術(shù)進(jìn)行了深入探討。論文的主要成果和創(chuàng)新點(diǎn)有:
　　(1)通過集成規(guī)范管

3、理、形式化建模以及驗(yàn)證等多種技術(shù)手段，改進(jìn)了當(dāng)前的列控系統(tǒng)需求規(guī)范建模與驗(yàn)證方法。與其它建模與驗(yàn)證方法只能針對(duì)系統(tǒng)需求規(guī)范的某一場(chǎng)景或某種單一特性不同，該方法能夠適用于整個(gè)列控系統(tǒng)需求規(guī)范。
　　(2)針對(duì)列控系統(tǒng)需求規(guī)范的特點(diǎn)，在列控系統(tǒng)需求規(guī)范形式化建模與驗(yàn)證方法中強(qiáng)化了安全規(guī)范要素，通過映射關(guān)系，用形式化方法將安全要素融入規(guī)范模型中。同時(shí)，建立了相對(duì)完整的追蹤與反饋機(jī)制，有助于研究人員對(duì)自然語言系統(tǒng)需求規(guī)范與模型進(jìn)行一致性和

4、覆蓋性進(jìn)行分析，并且能夠?qū)崿F(xiàn)建模模型與驗(yàn)證模型的轉(zhuǎn)換以及對(duì)驗(yàn)證結(jié)果的分析，從而使驗(yàn)證結(jié)果能夠利用反饋機(jī)制追蹤至規(guī)范文檔。
　　(3)建立了基于擴(kuò)展UML的列控系統(tǒng)需求規(guī)范建模方法，給出了列控系統(tǒng)需求規(guī)范建模模板，模板中的構(gòu)造型、標(biāo)記值及約束刻畫了系統(tǒng)需求規(guī)范中主要的強(qiáng)制性安全需求，使模型能夠體現(xiàn)系統(tǒng)的安全特性，并且增強(qiáng)了模型的可重用性，提高了建模的效率。另一方面，細(xì)化了規(guī)范建模和模型檢查規(guī)則，明確定義了列控系統(tǒng)需求規(guī)范片段的分類方

5、法以及規(guī)范與模型的映射方式。這些規(guī)則的建立，能夠大大減少建模人員在建模過程中的主觀因素。
　　(4)提出了UML模型轉(zhuǎn)換成CSP模型的方法，分別建立了UML和CSP的元模型，通過分析源元模型和目標(biāo)元模型語言的特征，建立了一組模型轉(zhuǎn)換規(guī)則，以實(shí)現(xiàn)原子映射和模式映射。為了保證嚴(yán)謹(jǐn)而科學(xué)的模型轉(zhuǎn)換過程，探討了模型轉(zhuǎn)換中特性的保持及轉(zhuǎn)換規(guī)則正確性的證明方法。
　　(5)設(shè)計(jì)并實(shí)現(xiàn)了列控系統(tǒng)需求規(guī)范形式化建模與驗(yàn)證軟件工具。該軟件工具