屬性驅(qū)動(dòng)的列車控制系統(tǒng)需求建模與驗(yàn)證

何麗蕓，趙 林，程瑞軍

（北京交通大學(xué) 軌道交通控制與安全國家重點(diǎn)實(shí)驗(yàn)室，北京 100044）

屬性驅(qū)動(dòng)的列車控制系統(tǒng)需求建模與驗(yàn)證

何麗蕓，趙 林，程瑞軍

（北京交通大學(xué) 軌道交通控制與安全國家重點(diǎn)實(shí)驗(yàn)室，北京 100044）

形式化語言越來越多地用來描述列車控制系統(tǒng)需求規(guī)范，其精確的語法和語義一方面有助于創(chuàng)建精確的需求模型、消除理解差異，另一方面也為進(jìn)一步分析驗(yàn)證提供了基礎(chǔ)。通過提出一種基于屬性的需求分析方法，利用具體的形式化技術(shù)來分析需求。首先將由自然語言描述的需求規(guī)范轉(zhuǎn)換為屬性描述語言（PSL）形式化規(guī)范，并通過仿真和博弈分別進(jìn)行語義檢查和可實(shí)現(xiàn)性驗(yàn)證，最后通過斷言來檢驗(yàn)形式化語言所刻畫的系統(tǒng)的精確性和完整性。該方法從自然語言形式的需求約束中直接提取相關(guān)需求規(guī)范，構(gòu)造形式化模型并進(jìn)行驗(yàn)證，為需求的早期確認(rèn)提供了一種新的實(shí)用途徑。并以CTCS-3級(jí)列控系統(tǒng)RBC切換場(chǎng)景為例，說明該方法的有效性。

需求規(guī)范；驗(yàn)證；列車控制系統(tǒng)；仿真；可實(shí)現(xiàn)性

需求規(guī)范是系統(tǒng)開發(fā)重要的依據(jù)性規(guī)范標(biāo)準(zhǔn)。高質(zhì)量的需求規(guī)范可以切斷需求階段的bug來源，如果需求規(guī)范的質(zhì)量控制不到位，極有可能會(huì)產(chǎn)生最原始的bug，并將會(huì)貫穿到整個(gè)系統(tǒng)開發(fā)的始終，造成巨大的經(jīng)濟(jì)損失。工業(yè)數(shù)據(jù)顯示大約50%的產(chǎn)品缺陷是由于需求的質(zhì)量不到位造成的，大約80% 的返工工作量可以追溯到需求缺陷[1]，特別是對(duì)列車運(yùn)行控制系統(tǒng)（以下簡(jiǎn)稱“列控系統(tǒng)”）而言，其需求規(guī)范的缺陷往往造成不可估量的財(cái)產(chǎn)損失和人員傷亡。具體來說，列控系統(tǒng)需求規(guī)范大多都是依靠領(lǐng)域?qū)＜覀兊慕?jīng)驗(yàn)而制定的，不可避免地存在某些漏洞或者安全隱患；另外，用自然語言刻畫的系統(tǒng)需求規(guī)范可能存在歧義。這都將會(huì)給系統(tǒng)的設(shè)計(jì)與開發(fā)帶來不利影響。因此，在列控系統(tǒng)開發(fā)的早期階段對(duì)需求進(jìn)行形式化分析驗(yàn)證以保證需求質(zhì)量顯得十分必要。

列車運(yùn)行控制系統(tǒng)是安全苛求系統(tǒng)。根據(jù)鐵路工業(yè)標(biāo)準(zhǔn)（CENELEC EN50128[2]）和國際通用的安全相關(guān)系統(tǒng)標(biāo)準(zhǔn)（IEC61508[3]），對(duì)高安全系統(tǒng)（安全完善度等級(jí)4級(jí)），強(qiáng)烈推薦使用形式化方法對(duì)系統(tǒng)需求進(jìn)行分析驗(yàn)證。形式化方法[4]是采用嚴(yán)格的數(shù)學(xué)語言、具有精確的數(shù)學(xué)語義的方法，適合于軟件和硬件系統(tǒng)的描述、開發(fā)和驗(yàn)證。屬性描述語言（PSL）[5]作為一種形式化的屬性規(guī)范語言，易于讀寫、語法精簡(jiǎn)、語義嚴(yán)格清晰。利用PSL語言表達(dá)需求，使得需求以唯一的方式被解釋，能夠排除由自然語言帶來地二義性，進(jìn)而準(zhǔn)確地表達(dá)需求。

因此，本文以PSL語言為基礎(chǔ)，提出了一種基于屬性的需求分析方法，該方法可以從自然語言形式的需求約束中直接提取和構(gòu)造形式化模型，通過對(duì)形式化模型進(jìn)行仿真（Simulation）、博弈（Game）、以及斷言（Assurance）來分析需求，確保形式化需求的語義正確性、完整性以及可實(shí)現(xiàn)性。其中，設(shè)計(jì)人員可以通過屬性仿真來構(gòu)建具體的場(chǎng)景并檢驗(yàn)?zāi)硞€(gè)屬性所刻畫的行為是否符合需求規(guī)范約束；通過博弈來對(duì)形式化模型進(jìn)行可實(shí)現(xiàn)性驗(yàn)證；通過屬性斷言從更全面整體的角度來分析形式化模型，驗(yàn)證形式化屬性集是否一致，是否足夠完整地刻畫一個(gè)系統(tǒng)的行為。從而可以有效地解決需求規(guī)范的表意模糊和邏輯缺陷問題，并且能夠在系統(tǒng)開發(fā)的初期對(duì)規(guī)范中的漏洞進(jìn)行排查，提高需求的質(zhì)量。最后，本文以列控系統(tǒng)的無線閉塞中心（RBC）切換場(chǎng)景[6]為例來說明該方法的有效性。

1 基于屬性的需求分析方法

基于屬性的需求分析方法通過屬性仿真、屬性斷言和博弈來對(duì)系統(tǒng)需求的一致性、完整性以及可實(shí)現(xiàn)性進(jìn)行驗(yàn)證分析，是一個(gè)不斷迭代的過程。圖1描述了基于屬性的需求分析過程。

如圖1所示，設(shè)計(jì)人員首先從自然語言描述的用戶需求或未經(jīng)驗(yàn)證完善的需求規(guī)范中提取和構(gòu)建形式化模型，通過屬性仿真來探索和研究形式化屬性的語義，將屬性的形式化表達(dá)式逐級(jí)分解來使設(shè)計(jì)人員更好地理解表達(dá)式，也可以用來糾正PSL形式化屬性表達(dá)式的錯(cuò)誤；通過博弈來分析所刻畫的系統(tǒng)是否存在，是否可實(shí)現(xiàn)；通過屬性斷言對(duì)形式化需求規(guī)范的一致性和完整性檢查。其主要步驟簡(jiǎn)述如下：

圖1 基于屬性的需求分析過程

（1）從自然語言描述的用戶需求或未經(jīng)驗(yàn)證完善的需求規(guī)范約束中直接提取和構(gòu)建形式化需求模型Γ，該形式化需求模型使用PSL表示。對(duì)需求模型Γ進(jìn)行一致性檢查，保證需求模型中的需求之間不存在沖突。

（2）若需求一致，則通過仿真來逐條檢驗(yàn)需求模型Γ的形式化表達(dá)是否正確，是否描述的是所期望的行為，從而糾正并探索PSL形式化屬性表達(dá)式的語義。

（3）檢查由需求模型Γ所刻畫的系統(tǒng)是否為可實(shí)現(xiàn)，即是否存在與之相一致的系統(tǒng)。需求模型Γ中的變量分為環(huán)境（不可控）變量和系統(tǒng)（可控）變量。需求包含假定（Assumptions）需求和保證（Guarantees）需求兩種類型，分別是對(duì)環(huán)境變?chǔ)樟亢拖到y(tǒng)變量的約束。當(dāng)環(huán)境輸入變量滿足所有假定需求時(shí)，存在一組滿足所有保證需求的系統(tǒng)變量，則稱該規(guī)范是可實(shí)現(xiàn)的。否則，規(guī)范為不可實(shí)現(xiàn)，需進(jìn)行調(diào)試并修改該需求集。

（4）若系統(tǒng)可實(shí)現(xiàn)，則對(duì)形式化模型進(jìn)行基于斷言的驗(yàn)證，即通過兩個(gè)屬性集：assertionsφA和possibilities φP分別進(jìn)行驗(yàn)證。assertions φA，驗(yàn)證所構(gòu)建的形式化模型是否一定滿足assertions屬性，通過assertions來檢查形式化模型是否約束不足。possibilities φP，驗(yàn)證形式化模型是否存在滿足possibilities屬性的可能性，通過possibilities來檢查需求是否約束過強(qiáng)。

（5）如果不滿足φA，檢查需求模型Γ是否約束不足，是否需要增加系統(tǒng)行為約束。如果不滿足φP，檢查需求模型Γ是否約束過強(qiáng)，是否需要去除系統(tǒng)行為的某個(gè)約束。通過這種方法，對(duì)需求模型Γ檢查修改，保證形式化需求模型的正確性。

（6）通過對(duì)需求模型Γ的修改更新，使其均滿足φA和φP后，逐步增加兩個(gè)屬性集φA和φP中的屬性約束再進(jìn)行驗(yàn)證，轉(zhuǎn)到第一步，不斷迭代，從而豐富和完善對(duì)系統(tǒng)的屬性刻畫。

為了形象地說明基于屬性的需求分析，將其用一個(gè)三元組來表示：

其中：

Γ： 形式化需求模型，描述系統(tǒng)行為和環(huán)境行為。Γ=＜S,E,RG,RA＞，其中，S和E是變量的兩個(gè)不相交集，S代表系統(tǒng)變量（受系統(tǒng)控制的變量），E代表環(huán)境變量（受環(huán)境控制的變量）。需求分為Guarantee需求和Assumption需求。Guarantee需求用RG表示，是關(guān)于系統(tǒng)變量的PSL屬性集；Assumption需求用RA表示，是關(guān)于環(huán)境變量的PSL屬性集。

φA：assertions屬性集，用Γ來描述的系統(tǒng)行為必須保證滿足assertion屬性（系統(tǒng)屬性的所有路徑必須都滿足assertions屬性集），通過assertions來檢查需求是否約束不足。

φP：possibilities屬性集，用Γ來描述的系統(tǒng)行為允許possibilities屬性（系統(tǒng)屬性中存在一條路徑滿足possibilities屬性），通過possibilitie來檢查需求是否約束過強(qiáng)。

下面以仲裁器為例進(jìn)行說明，仲裁器的部分需求表示如下：

其中，g1和g2是布爾型系統(tǒng)變量，表示總線授權(quán)給出響應(yīng)。r1和r2是布爾型環(huán)境變量，表示對(duì)總線發(fā)送請(qǐng)求。RG1表示兩個(gè)請(qǐng)求信號(hào)不能同時(shí)得到響應(yīng)，RG2表示有請(qǐng)求最終會(huì)有響應(yīng)，當(dāng)S滿足RG時(shí)，E滿足RA，則系統(tǒng)是可實(shí)現(xiàn)的。同時(shí)，通過φA和φP來檢驗(yàn)需求模型是否正確完整。

RATSY（ Requirements Analysis Tool with Synthesis[7]）是一種基于屬性的需求分析工具，它為工程人員提供了仿真、斷言和可實(shí)現(xiàn)性驗(yàn)證的環(huán)境。以PSL為輸入語言，避免了復(fù)雜的建模過程，對(duì)獲得正確的形式化需求規(guī)范起到重要作用。下面以RBC切換場(chǎng)景為例說明基于屬性的需求分析方法在列控領(lǐng)域中的應(yīng)用。

2 基于屬性的需求分析方法在列控系統(tǒng)需求規(guī)范中的應(yīng)用

CTCS-3級(jí)列控系統(tǒng)是基于全球鐵路移動(dòng)通信系統(tǒng)（GSM-R）的列車運(yùn)行控制系統(tǒng),通過車-地信息的雙向傳輸實(shí)現(xiàn)列車的閉環(huán)控制, 有效地提高列車的運(yùn)營效率。由于包含有大量的子系統(tǒng)且功能復(fù)雜，在開發(fā)過程中，正確地理解并建立系統(tǒng)需求規(guī)范是首要問題。盡管工業(yè)數(shù)據(jù)顯示大約50%的產(chǎn)品缺陷是由于需求的質(zhì)量不到位造成的，大約80%的返工工作量可以追溯到需求缺陷，但是對(duì)需求的分析手段卻很缺乏，而借助計(jì)算機(jī)輔助分析手段建立形式化的需求規(guī)范是一種有效的途徑。下面以RBC切換場(chǎng)景為例進(jìn)行說明。

2.1 形式化需求模型的建立

場(chǎng)景可以用作分析與驗(yàn)證需求的有效工具，可以通過選擇一組具有代表性的場(chǎng)景實(shí)例來對(duì)屬性需求進(jìn)行檢驗(yàn)，以發(fā)現(xiàn)需求中存在的缺陷。一組具有代表性的場(chǎng)景實(shí)例應(yīng)該既包含描述一些系統(tǒng)期望行為的場(chǎng)景，即期望場(chǎng)景，也包含描述一些系統(tǒng)不希望發(fā)生行為的場(chǎng)景，即異常場(chǎng)景。使用場(chǎng)景實(shí)例對(duì)需求進(jìn)行驗(yàn)證和校驗(yàn)，期望場(chǎng)景可以驗(yàn)證需求的完整性，異常場(chǎng)景可以驗(yàn)證需求的正確性。

CTCS-3級(jí)列控系統(tǒng)主要運(yùn)營場(chǎng)景包括注冊(cè)與啟動(dòng)、注銷、進(jìn)出動(dòng)車段、等級(jí)轉(zhuǎn)換、行車許可、RBC切換、自動(dòng)過分相、重聯(lián)和摘解、臨時(shí)限速、降級(jí)情況、災(zāi)害防護(hù)、調(diào)車作業(yè)、人工解鎖進(jìn)路、特殊進(jìn)路共14個(gè)場(chǎng)景文件，其中RBC場(chǎng)景是CTCS-3級(jí)列控系統(tǒng)中最為重要和最具代表性的流程之一，

現(xiàn)對(duì)該場(chǎng)景需求進(jìn)行分析研究。場(chǎng)景中表示的屬性含義參見表1。

表1 場(chǎng)景中各屬性的含義

為了敘述簡(jiǎn)單清晰，根據(jù)CTCS-3級(jí)列控需求規(guī)范，提取RBC切換運(yùn)營場(chǎng)景的部分片段（兩部電臺(tái)都能進(jìn)行正常的RBC切換）進(jìn)行分析，以車載設(shè)備為系統(tǒng)，其他均看作環(huán)境。構(gòu)建一個(gè)初步的形式化需求模型，該模型用形式化語言PSL表述如下：

RG1：允許車載設(shè)備與RBC 通信中斷的時(shí)間為7 s～20 s，當(dāng)超過這段時(shí)間則降級(jí)處理。always(CommunicationInterrupt=1&&C3=1-＞next (C2=1))

RG2：如果車載設(shè)備的版本與RBC的版本不兼容，則觸發(fā)車載設(shè)備降級(jí)運(yùn)行。

always(ID_RBCincompatible=1&&C3=1-＞next(C2=1))

RG3：當(dāng)列車運(yùn)行速度超過最大速度曲線規(guī)定的速度時(shí)，C3控制單元應(yīng)能通過安全數(shù)字接口實(shí)現(xiàn)安全防護(hù)（超速時(shí)應(yīng)能實(shí)現(xiàn)安全防護(hù)）。

always(OverSpeed=1-＞next(SafetyProtection=1))

RG4：當(dāng)車載設(shè)備(OBE)正常運(yùn)行無故障時(shí)，應(yīng)能實(shí)現(xiàn)通信、安全防護(hù)、監(jiān)控、制動(dòng)和計(jì)算的功能。

always(OBE_faultFree＜_＞(!CommunicationIn terrupt&&SafetyProtection&&Supervision&&Brak e&&

Compute))

RG5：車載設(shè)備應(yīng)處于CTCS-2或CTCS-3級(jí)運(yùn)行，同時(shí)CTCS-2和CTCS-3級(jí)互斥。

always((C3=1&&C2=0)||(C3=0&&C2=1))

RG6：如果通信不中斷且列車處于CTCS-3級(jí)運(yùn)行，則繼續(xù)以CTCS-3級(jí)運(yùn)行。

always(CommunicationInterrupt=0&&C3=1-＞next (C3=1))

RA1：預(yù)告點(diǎn)（LTA）到切換點(diǎn)（RN）應(yīng)滿足列車不小于40 s的運(yùn)行距離。

always(LTA=1_＞next[40](RN=1))

RA2：當(dāng)列車前端通過RN時(shí)，“移交RBC”停止對(duì)列車的控制，切換到“接收RBC”進(jìn)行控制。

always(RN=1_＞next(HandoverRBC_MA=0& &AcceptRBC_MA=1))

RA3：列車不能同時(shí)使用“移交RBC”發(fā)送的行車許可和“接收RBC”發(fā)送的行車許可。

never(HandoverRBC_MA&&AcceptRBC_MA)

RA4：為消除RBC切換對(duì)列車正常運(yùn)行的影響，車載設(shè)備應(yīng)設(shè)置兩部獨(dú)立GSM-R通信電臺(tái)（GSM-R1和GSM-R2），車載設(shè)備通過GSM-R1接收“移交RBC” 發(fā)送的MA，通過GSM-R2呼叫“接收RBC”。

(always(HandoverRBC_MA＜-＞GSMR1))&&(always(AcceptRBC_MA＜-＞GSM-R2))

RBC切換描述了在不同RBC邊界處，實(shí)現(xiàn)列車在兩個(gè)RBC間行車許可控制的安全切換過程。通過上述的轉(zhuǎn)化，初步得到一個(gè)形式化的需求規(guī)范如下：

PARBCTransition=＜Γ,φA,φP＞

其中，

S ={C3, C2, Speed_c2, Speed_c3,

OverSpeed, SafetyProtection, OBE_faultFree, SafetyProtection, Supervision, Brake, Compute }

E={CommunicationInterrupt, ID_RBCincompatible, LTA, RN, HandoverRBC _MA,AcceptRBC_MA, GSM-R1, GSM-R2 }

2.2 形式化模型的仿真、可實(shí)現(xiàn)性驗(yàn)證及斷言

2.2.1 形式化需求的仿真

利用形式化屬性成功地刻畫系統(tǒng)的一個(gè)先決條件是對(duì)屬性語言要有一個(gè)正確的理解。RATSY提供的屬性仿真環(huán)境使得工程人員可以逐條對(duì)屬性約束的正確性進(jìn)行確認(rèn)，從而判斷該屬性所描述的行為是不是我們所期望。例如，對(duì)屬性RA2: always(RN-＞next(!HandoverRBC_MA&&AcceptRBC_MA))進(jìn)行語義檢驗(yàn)。仿真結(jié)果如圖2所示，給出正例（RA2所描述的需求成立）和反例（RA2所描述的需求不成立），更好地理解滿足屬性RA2或違反屬性RA2的情況。

圖2 屬性仿真

2.2.2 形式化需求模型的可實(shí)現(xiàn)性驗(yàn)證

在保證需求模型中的每條需求約束都正確后，開始從整體上對(duì)形式化模型進(jìn)行可實(shí)現(xiàn)性驗(yàn)證。也就是說，當(dāng)所有的環(huán)境變量滿足Assumption需求時(shí)，所有的系統(tǒng)變量也滿足Guarantee需求。只有保證需求模型是可實(shí)現(xiàn)的，后面的斷言驗(yàn)證才有意義。通過驗(yàn)證，上面的需求是不可實(shí)現(xiàn)的。為了更加方便快速地找到需求不可實(shí)現(xiàn)的原因，工具為工程人員提供了診斷信息并且將與該系統(tǒng)不可實(shí)現(xiàn)有關(guān)的需求做標(biāo)記。如圖3所示，需求RG1、需求RG2、需求RG3、需求RG4以及需求RG6與系統(tǒng)的不可實(shí)現(xiàn)有關(guān)。RG6表示如果通信不中斷且列車處于C3級(jí)運(yùn)行，則繼續(xù)以C3級(jí)運(yùn)行，而RG2表示如果車載設(shè)備的版本與RBC的版本不兼容，則觸發(fā)車載設(shè)備降級(jí)運(yùn)行?？梢妰烧叽嬖诿埽瑧?yīng)在通信不中斷并且車載設(shè)備的版本與RBC的版本兼容時(shí)，系統(tǒng)才可能以C3級(jí)正常運(yùn)行。因此，對(duì)RG6進(jìn)一步約束為：always(CommunicationInte rrupt=0&&C3=1&&ID_RBCincompatible=0_＞next( C3=1))。驗(yàn)證修正后的需求模型是可實(shí)現(xiàn)的?；趯傩缘男枨蠓治龇椒槲覀儾檎译[藏在需求中的可實(shí)現(xiàn)性問題提供了一種快捷而有效的手段。

圖3 GAME窗口

2.2.3 形式化需求模型基于斷言的驗(yàn)證

雖然我們保證了需求集的可實(shí)現(xiàn)性和屬性語義正確性，但是這對(duì)于刻畫一個(gè)完整而正確的系統(tǒng)是遠(yuǎn)遠(yuǎn)不夠的，通過基于斷言的驗(yàn)證來保證需求的完整性以及需求約束程度的合理性，約束不能過強(qiáng)或者不足。

前面所給的形式化模型中φA為空集，現(xiàn)在假定φA={a1, a2}并進(jìn)行驗(yàn)證，其中：

a1：當(dāng)車載設(shè)備通過兩部電臺(tái)與RBC1和RBC2同時(shí)進(jìn)行連接通信時(shí)，如果司機(jī)關(guān)閉了駕駛臺(tái)，車載設(shè)備將對(duì)RBC1和RBC2都執(zhí)行終止任務(wù)程序。

always(DeskClosed=1-＞next(Handover-RBC_MA=0&&AcceptRBC_MA=0))

a2：如果列車位置信息無效，則降級(jí)，列車?yán)^續(xù)保持與RBC的通信會(huì)話

always(TrainLocation=0-＞next(C2=1))

驗(yàn)證結(jié)果如圖4所示，需求集Γ=＜S,E,A,G＞不能滿足φA屬性，說明需求Γ約束不夠，將a1和a2分別加入需求集Γ中，從而更新了需求集合，增強(qiáng)了對(duì)系統(tǒng)屬性的約束，使得系統(tǒng)屬性表示更加準(zhǔn)確。

圖4 驗(yàn)證結(jié)果

對(duì)φP集驗(yàn)證的意義不同于φA的驗(yàn)證，φA所描述的屬性需求集Γ的所有路徑必須都滿足。而φP中的屬性需求集Γ只要存在一條路徑滿足即可，保證了需求集約束的精確程度，不會(huì)因?yàn)榧s束過緊或約束不夠而影響所刻畫系統(tǒng)的準(zhǔn)確性。在這里，φP={p1 },其中：

p1: 當(dāng)列車RBC切換點(diǎn)時(shí)，通信中斷，列車不能得到移交RBC和接收RBC的行車許可。

always(RN=1&&CommunicationInterrupt=0_＞next(HandoverRBC_MA=0&&AcceptRBC_MA= 0))。

驗(yàn)證結(jié)果表明，需求模型所刻畫的系統(tǒng)滿足p1屬性，與我們的設(shè)計(jì)意圖相符，說明需求約束并不存在過強(qiáng)的問題。

運(yùn)用上面的方法進(jìn)行不斷迭代，發(fā)現(xiàn)列控需求規(guī)范中的缺陷和漏洞，例如某條需求可能存在約束不夠或約束過強(qiáng)的問題，從而獲得高質(zhì)量的需求，也保證了生命財(cái)產(chǎn)的安全。

3 結(jié)束語

本文所提出的基于屬性的需求分析方法通過驗(yàn)證需求的正確性、完整性以及可實(shí)現(xiàn)性，可以有效地解決需求規(guī)范的表意模糊和邏輯缺陷問題，并且能夠在系統(tǒng)開發(fā)的初期對(duì)規(guī)范中的漏洞進(jìn)行排查，提高需求的質(zhì)量。采用該方法將PSL與可視化界面工具RATSY相結(jié)合，對(duì)高安全要求的列控系統(tǒng)需求規(guī)范進(jìn)行分析驗(yàn)證，通過反例對(duì)錯(cuò)誤進(jìn)行定位和修改。驗(yàn)證過程表明，基于屬性的需求分析方法適用于CTCS-3級(jí)列控系統(tǒng)需求規(guī)范的分析驗(yàn)證。該方法簡(jiǎn)便易行，避免了復(fù)雜的建模和轉(zhuǎn)換過程。對(duì)于初步編寫規(guī)范及對(duì)原有系統(tǒng)規(guī)范進(jìn)行更新升級(jí)的工作具有重要的意義。

[1] 常云麗,鄔欣明,鄭 威.軍用軟件需求分析研究[J].火力與指揮控制，2013，38（1）.

[2] CELENEC EN 50128: Railway Applications - Communications, signaling and processing systems- Software for railway control and protection systems[S]. 2001.

[3] International Standard IEC 61508: Functional Safety of Elec

trical/Electronic/Programmable Electronic SafetyRelated Sys

tems. International Electrotechnical Commission[S]. 2000. [4] 包麗梅,張玉春,張世錚.關(guān)于形式化方法與軟件可靠性的研究[J].內(nèi)蒙古民族大學(xué)學(xué)報(bào)：自然科學(xué)版，2010（2）：166-167.

[5] Accellera. Property specif i cation language reference manual version 1.1[EB/OL]. (2004-06-09)[2008-03-02]. http://www. eda.org/vfv/docs/PSL-v1.1.pdf．

[6] 中華人民共和國鐵道部. CTCS-3級(jí)列控系統(tǒng)系統(tǒng)需求規(guī)范(SRS)[M]. 北京：中國鐵道出版社，2009.

[7] Bloem R, Cavada R, Cimatti A ,et al. RATSY-A new Requirements Analysis Tool withSynthesis[C].Computer Aided Veri-f i cation, 22nd International Conference. Berlin:Springer-Verlag, 2010: 425-429.

責(zé)任編輯 楊利明

Property-driven modeling and verif i cation for requirements of Train Control System

HE Liyun, ZHAO Lin, CHENG Ruijun
( State Key Laboratory of Rail Traff i c Control and Safety, Beijing Jiaotong University, Beijing 100044, China )

Formal languages were increasingly used to describe the requirements specif i cation of Train Control System, the precise syntax and semantics on the one hand, helped to create accurate demand model, eliminated understanding differences, on the other hand also provided a basis for further analysis of the validation. This paper presented a property based requirements analysis approach which analyzed requirement by the application of specialized formal analysis techniques. Firstly, requirements described by natural language were transformed into formal requirements described by PSL (Property Specification Language). Secondly, the semantics were checked by simulation and the realizability of the System was verif i ed by the game. Finally, the correctness and completeness of the System were validated by assurance. This method directly extracted the relative requirements specif i cation from requirement constraints described by natural language and formalized the structures model to verify, also provided a new practical way for the early validation of the requirements. By using some requirement fragments from RBC Handover scenarios of CTCS-3 Train Control System as a realistic example, it was demonstrated the effectiveness of this approach.

requirements specif i cation; verif i cation; Train Control System; simulation; realizability

U284.4∶TP39

A

1005-8451（2014）02-0001-06

2013-11-06

國家國際科技合作專項(xiàng)項(xiàng)目（2012DFG81600）；北京交通大學(xué)軌道交通控制與安全國家重點(diǎn)實(shí)驗(yàn)室自主課題項(xiàng)目（No.RCS2012ZT006）。

何麗蕓，在讀碩士研究生；趙 林，講師。