應(yīng)答器報文編制規(guī)則的形式化建模與驗證

黃 旭，劉中田

(1. 中鐵第一勘察設(shè)計院集團有限公司， 陜西西安 710043; 2. 北京交通大學電子信息工程學院，北京 100044)

應(yīng)答器作為列車控制系統(tǒng)中必不可少的設(shè)備，其向車載設(shè)備傳輸?shù)膱笪臄?shù)據(jù)是生成控車曲線的依據(jù)。CTCS-2級應(yīng)答器報文直接用于ATP控車，應(yīng)答器報文編制錯誤可能導致列車超速或冒進，嚴重影響列車運行安全。當前應(yīng)答器報文生成過程為：“列控數(shù)據(jù)-用戶報文-傳輸報文”。從列控數(shù)據(jù)到用戶報文的過程通常是基于《CTCS-2級列控系統(tǒng)應(yīng)答器應(yīng)用原則》[1](以下簡稱應(yīng)答器應(yīng)用原則)和《列控數(shù)據(jù)管理暫行辦法》[2]直接編寫軟件經(jīng)人工操作來完成，用戶報文到傳輸報文的編碼依據(jù)是行業(yè)規(guī)范SUBSET-036[3]。應(yīng)答器應(yīng)用原則是編制應(yīng)答器報文的標準規(guī)范，報文數(shù)據(jù)的正確性與應(yīng)用原則的正確性及其被正確理解和應(yīng)用息息相關(guān)，但應(yīng)用原則存在兩個問題：(1)應(yīng)答器應(yīng)用原則只規(guī)定應(yīng)答器的設(shè)置原則和報文的結(jié)構(gòu)等內(nèi)容，沒有描述具體的編制報文規(guī)則，完備性不足。(2)基于文本語言描述的應(yīng)答器應(yīng)用原則易產(chǎn)生二義性問題，存在較大隱患。針對這兩個問題，需要對應(yīng)答器應(yīng)用原則分析整理，得到明確的報文編制規(guī)則以解決完備性問題；對于文本語言描述產(chǎn)生二義性的問題，可采用形式化方法來描述應(yīng)用原則，使得應(yīng)用原則以唯一的方式被解釋，可以有效排除自然語言的二義性，且形式化的描述為進一步形式化分析和驗證提供了可能性，這對確保應(yīng)答器報文正確性有重要意義。

對于列控數(shù)據(jù)的安全性，文獻[4]對各類列控數(shù)據(jù)間的約束關(guān)系進行了深入研究，提取了驗證列控數(shù)據(jù)的邏輯規(guī)則，并證明了所提取規(guī)則的可滿足性，對確保列控數(shù)據(jù)的正確性有重要的作用。文獻[5-6]對用戶報文到傳輸報文的編碼過程及方法進行深入研究，使得這一環(huán)節(jié)的安全性有所保障。而“列控數(shù)據(jù)-用戶報文”這一環(huán)節(jié)缺乏嚴格和深入的理論研究。目前國內(nèi)外對應(yīng)答器報文編制規(guī)則的研究較少，相關(guān)研究有從工程實施角度對應(yīng)答器應(yīng)用原則部分內(nèi)容進行分析，對報文發(fā)送原則提出優(yōu)化措施[7]，還有針對應(yīng)答器布置階段，用數(shù)學語言對應(yīng)答器應(yīng)用方案進行描述，并結(jié)合應(yīng)答器應(yīng)用原則提出一套應(yīng)答器應(yīng)用方案的驗證和優(yōu)化方法[8]。已有的研究均是在已有應(yīng)答器應(yīng)用原則的基礎(chǔ)上對其從經(jīng)濟和工程的方面進行優(yōu)化改進，但均未從安全的視角對應(yīng)答器應(yīng)用原則進行研究。

列控系統(tǒng)是典型的復雜安全苛求系統(tǒng)，根據(jù)國際標準IEC 61508，對于高安全系統(tǒng)推薦使用形式化方法進行分析[9]，針對上述應(yīng)答器報文編制過程存在的問題，本文深度分析應(yīng)答器應(yīng)用原則中規(guī)定的各信息包之間的關(guān)聯(lián)關(guān)系，結(jié)合列控數(shù)據(jù)的格式，提取得到應(yīng)答器報文的編制規(guī)則。對于提取所得的應(yīng)答器報文編制規(guī)則，采用UML與NuSMV相結(jié)合的方法進行形式化建模與驗證，分析驗證結(jié)果，得到應(yīng)答器應(yīng)用原則存在的問題，并經(jīng)過反例追蹤、定位、修改和重新驗證應(yīng)用原則，可以得到報文編制規(guī)則的UML模型，有效避免了文本語言存在的二義性問題，這對提高報文的正確性有著積極的作用，也對保障列控系統(tǒng)的安全運行具有重要意義。

1 應(yīng)答器報文編制規(guī)則的提取

CTCS-2級列控系統(tǒng)應(yīng)答器應(yīng)用原則中[1]描述了應(yīng)答器報文結(jié)構(gòu)、用戶信息包變量的含義和不同用途應(yīng)答器所應(yīng)包含的報文內(nèi)容，但并未具體描述如何從列控數(shù)據(jù)中獲取得到報文，且應(yīng)答器應(yīng)用原則中存在較多模糊的描述，如5.3.11節(jié)中定位(DW)應(yīng)答器報文編制規(guī)則中ETCS-72包的數(shù)據(jù)范圍描述為“車站名稱提前三個閉塞分區(qū)顯示，列車越過出站口后停止顯示”，沒有具體說明數(shù)據(jù)起點和終點，只能憑借人工摸索。

列控數(shù)據(jù)主要由應(yīng)答器位置表、信號數(shù)據(jù)表、坡度表、速度表、分相信息表、線路斷鏈明細表、車站信息表等組成，分別對應(yīng)應(yīng)答器報文中不同的用戶信息包。本文根據(jù)應(yīng)答器報文中各用戶信息包之間的關(guān)聯(lián)關(guān)系，結(jié)合列控數(shù)據(jù)的內(nèi)容及格式，整理出應(yīng)答器報文編制規(guī)則，規(guī)則的整理思路如圖1所示。

圖1 應(yīng)答器報文編制規(guī)則的整理方法

將整理得到的規(guī)則總結(jié)為兩部分：一是確定用戶信息包種類，二是生成信息包內(nèi)容。以區(qū)間無源應(yīng)答器報文生成場景為例，表1為提取得到的報文編制規(guī)則示例。

2 基于UML-NuSMV形式化建模與驗證方法

UML(Unified Model Language)是一種統(tǒng)一建模語言，是對面向?qū)ο箝_發(fā)系統(tǒng)的產(chǎn)品進行說明、可視化和編制文檔的一種標準語言。UML直觀易懂的特點使其被廣泛應(yīng)用于各個行業(yè)。但其圖形化的符號缺乏精確的語義，并且缺乏分析驗證工具的支持[10]。

對比之下，形式化方法是以數(shù)學為基礎(chǔ)，用數(shù)學的方法來解決工程領(lǐng)域的問題，其目標是對系統(tǒng)建立精確的數(shù)學模型并對模型進行分析，在工業(yè)安全系統(tǒng)中已得到廣泛認可[11]。模型檢驗是一種自動驗證有窮狀態(tài)系統(tǒng)是否具有所期望的性質(zhì)的形式化方法[12-13]，其對應(yīng)的數(shù)學模型是有窮狀態(tài)系統(tǒng)；使用時態(tài)邏輯語言對期望的系統(tǒng)性質(zhì)進行描述；自動驗證的方法是遍歷有窮狀態(tài)系統(tǒng)的每一個狀態(tài)，最終給出系統(tǒng)模型是否具有期望性質(zhì)的結(jié)論[13]。NuSMV (New Symbolic Model Verifier)是新型的符號模型檢驗工具，用以檢測一個有窮系統(tǒng)是否滿足指定的性質(zhì)，支持計算樹邏輯和線性時序邏輯描述系統(tǒng)性質(zhì)，若不滿足則給出反例，用于回溯定位驗證結(jié)果。

表1 應(yīng)答器報文編制規(guī)則示例

本文對應(yīng)答器報文編制規(guī)則建模的驗證使用UML與NuSMV相結(jié)合的方法，如圖2所示。

(1)規(guī)則管理階段

對提取所得的應(yīng)答器報文編制規(guī)則進行管理，確保后續(xù)模型與規(guī)則的一致性和覆蓋性。

(2)建模階段

基于特定場景建立應(yīng)答器報文編制規(guī)則UML模型，并對UML模型進行擴展與抽象，隨后將規(guī)則的UML模型轉(zhuǎn)換為NuSMV語言模型；基于規(guī)則管理的結(jié)果，用時序邏輯來刻畫編制規(guī)則應(yīng)滿足的性質(zhì)，將兩部分輸入作為模型檢驗工具。

(3)模型驗證階段

模型檢驗工具NuSMV遍歷搜索輸入的有窮狀態(tài)系統(tǒng)模型，檢驗系統(tǒng)模型是否滿足指定的性質(zhì)。

(4)模型檢驗結(jié)果分析

若系統(tǒng)不滿足指定的性質(zhì)，則根據(jù)反例驗證結(jié)果對錯誤進行回溯、定位、修改和重新驗證。

2.1 面向NuSMV的UML建模

基于整理后的報文編制規(guī)則，建立編制規(guī)則的UML類圖、狀態(tài)轉(zhuǎn)移圖。UML類圖是用類及其相互關(guān)系對系統(tǒng)進行靜態(tài)描述。UML狀態(tài)圖是對系統(tǒng)動態(tài)行為建模，描述對象的不同狀態(tài)之間轉(zhuǎn)換的條件和響應(yīng)。報文編制規(guī)則對應(yīng)的UML模型中包含大量與驗證系統(tǒng)特性無關(guān)的數(shù)據(jù)，如果用NuSMV直接遍歷這些數(shù)據(jù)，會大幅增大系統(tǒng)的狀態(tài)空間，甚至會引發(fā)狀態(tài)爆炸。因此為了確保系統(tǒng)模型的可驗證性和驗證過程的高效性，需對報文編制規(guī)則的UML模型進行擴展和抽象。

(1)面向NuSMV的UML模型擴展

事件是一種允許系統(tǒng)對象和外界交互的消息機制，本文結(jié)合NuSMV的特性，在UML的基礎(chǔ)上引入輸入輸出事件，用布爾型數(shù)據(jù)代替字符型或整型數(shù)據(jù)。如報文編制規(guī)則中的應(yīng)答器組位置，編制規(guī)則需要得到的是該應(yīng)答器組的位置是否在分相區(qū)范圍內(nèi)，而應(yīng)答器組的坐標取值對于模型檢驗而言無任何意義，因此可引入“應(yīng)答器在分相區(qū)內(nèi)(Balise in_DZ)”事件，取值為1時表示本應(yīng)答器處在分相區(qū)范圍內(nèi)，取值為0則代表不在。

(2)面向NuSMV的UML模型抽象

完整的報文編制規(guī)則UML類圖中會存在大量與待檢驗系統(tǒng)性質(zhì)無關(guān)的特性和操作，抽象是一個緩解狀態(tài)問題最有效的方法之一，因此需要對原模型進行抽象，保留與待驗證性質(zhì)相關(guān)的變量即可。此過程應(yīng)根據(jù)影響錐COI(Cone of Influence)分析[14]，以確保抽象后的模型性質(zhì)能與原模型保持一致。

2.2 NuSMV建模

將2.1節(jié)中擴展和抽象后的UML模型轉(zhuǎn)換為NuSMV模型，轉(zhuǎn)換規(guī)則如下：

(1)NuSMV系統(tǒng)結(jié)構(gòu)

NuSMV程序語言由若干模塊(MODULE)組成，主要包括一個Main模塊和若干子模塊。其中Main模塊描述整個系統(tǒng)的組成以及待驗證的系統(tǒng)性質(zhì)，待驗證的系統(tǒng)性質(zhì)用SPEC關(guān)鍵字進行聲明，子模塊與UML中每個類意義對應(yīng)。

(2)MODULE部分

UML模型中每個類的輸入事件對應(yīng)相應(yīng)MODULE的形式化參數(shù)，并且在每個輸入事件前加前綴“in_”作為模塊輸入?yún)?shù)名，作用是使子模塊與主模塊關(guān)聯(lián)。

(3)VAR部分

變量聲明使用關(guān)鍵字VAR，主要用來創(chuàng)建組件關(guān)系、聲明模塊狀態(tài)機狀態(tài)和類的屬性。每個類的屬性轉(zhuǎn)換為對應(yīng)MODULE的VAR下的變量；每個屬性的數(shù)據(jù)類型轉(zhuǎn)換為對應(yīng)變量的數(shù)據(jù)類型；狀態(tài)機的狀態(tài)應(yīng)在VAR部分聲明。

(4)ASSIGN部分

變量賦值使用AGGGN關(guān)鍵字，主要用來說明狀態(tài)和屬性的初始變化以及變化機制。

具體NuSMV語言可以參考NuSMV指南和用戶手冊。

2.3 NuSMV模型檢驗及結(jié)果分析

2.3.1 模型檢驗

NuSMV模型檢驗使用特定的遍歷搜索算法來檢驗系統(tǒng)模型是否滿足指定的性質(zhì)，算法詳見文獻[15]。模型檢驗的基礎(chǔ)是將系統(tǒng)應(yīng)滿足的性質(zhì)用CTL(Computation Tree Logic)公式描述。 CTL由路徑謂詞和時態(tài)運算符兩部分構(gòu)成：路徑謂詞有兩類，分別是A(對所有路徑)和E(存在一個路徑)；時態(tài)運算符主要包括G,F,X,U， G(Goble)指所有狀態(tài)、F(Future)指未來的某個狀態(tài)、X(neXt)指下一個狀態(tài)、U(Until)指直到某一狀態(tài)。將系統(tǒng)性質(zhì)和系統(tǒng)模型輸入模型檢驗工具NuSMV進行模型檢驗。

(1)活性驗證

系統(tǒng)的活性是指從任何狀態(tài)系統(tǒng)都可以達到狀態(tài)s1。對應(yīng)驗證的CTL公式為：AG(EF(state=s1))。

(2)轉(zhuǎn)移性驗證

轉(zhuǎn)移性是指系統(tǒng)在狀態(tài)s1和狀態(tài)s2間可以互相轉(zhuǎn)移。對應(yīng)驗證的CTL公式為：EF(state=s1 & EX(state=s2))。

(3)反應(yīng)性驗證

說明R出現(xiàn)的條件，即表明S和R的因果關(guān)系；如果S出現(xiàn)，則R終將出現(xiàn)。驗證反應(yīng)性的CTL公式為：AG(S -> AF(R))。

CTL算子“->”關(guān)系真值表見表2。

(4)互斥性

互斥性是指系統(tǒng)的某兩個狀態(tài)一定不會同時出現(xiàn)。對應(yīng)驗證的CTL公式為：!EF(state=s1 & state=s2)。

(5)確定性驗證

表示系統(tǒng)不會同時處于狀態(tài)s1和狀態(tài)s2。與互斥性類似，但不同的是確定性對應(yīng)的是系統(tǒng)的無線運行狀態(tài)。驗證確定性的CTL公式為： !AG(state=s1 <-> state= s2)。

2.3.2 反例分析

對驗證結(jié)果進行分析，如果系統(tǒng)不滿足驗證性質(zhì)，NuSMV會給出反例來解釋邏輯公式不成立的原因。反例分析的方法是：按照反例提示，逐步檢查NuSMV系統(tǒng)建模、模型抽象、UML建模過程是否存在錯誤。如以上都無誤，最后確認所提取的報文編制規(guī)則是否存在問題或是應(yīng)用原則存在問題。如此逐步回溯定位，直至檢驗結(jié)果全部為TRUE或著找到應(yīng)用原則的問題。

3 報文編制規(guī)則的UML建模

針對報文編制規(guī)則的管理結(jié)果，本文以Q應(yīng)答器報文的生成場景為例，建立應(yīng)答器報文編制規(guī)則的UML類圖、時序圖和狀態(tài)圖。

3.1 UML類圖

采用面向?qū)ο蟮姆椒▽⒕幹埔?guī)則抽象為4個相互關(guān)聯(lián)的類，分別是信息包種類確定器類InfoTypeConfirmer、信息包內(nèi)容生成器類InfoContentCreater、列控數(shù)據(jù)類EngDataTables和用戶報文類UserDataPackets，其中信息包內(nèi)容生成器類包含了Head、E5、C1…等生成子類。圖3所示為擴展和抽象后的UML類圖，每個類都有其對應(yīng)的接收信息和輸出操作，接收信息以?signal?開頭，輸出操作以“+”開頭。例如InfoTypeConfirmer的接收信息有BaliseInfo()，輸出的操作是Con_E5()、Con_C1()等，具體字段含義見表3。

圖3 報文編制規(guī)則的UML類圖

名稱含義BaliseInfo()本應(yīng)答器組信息(位置,公里標,用途,類型,編號)N&S_BaliseInfo()下一組和第二組應(yīng)答器信息Last_BaliseInfo()上一組應(yīng)答器信息SecondQ()本應(yīng)答器前方第二個Q應(yīng)答器組公里標PosSignal_FJZFJZ信號機的公里標NextQ_FJZ本應(yīng)答器組前方的FJZ信號機外方第一個Q應(yīng)答器組信息DataScope()軌道區(qū)段數(shù)據(jù)范圍GradientInfo()數(shù)據(jù)范圍內(nèi)的坡度信息SpeedInfo()數(shù)據(jù)范圍內(nèi)的速度信息Con_E5(),Con_C1(),…確定包含E5、C1、…信息包Create_E5(),Create_C1(),…生成E5、C1、…信息包E5_Created(),C1_Created(),…E5、C1、…信息包已生成Find_Q_JZ()尋找JZ外方第一個和第二個Q應(yīng)答器組信息Find_DataScope1/2()尋找數(shù)據(jù)范圍(是/非JZ外方應(yīng)答器)TP1(2)()數(shù)據(jù)打靶點(是/非JZ外方應(yīng)答器)DZ_Info()分相區(qū)信息BD()列車的最大制動距離C1_LPACKERC1信息包位數(shù)

3.2 UML狀態(tài)轉(zhuǎn)移圖

狀態(tài)圖主要用來描述對象、子系統(tǒng)、系統(tǒng)的生命周期，模型檢驗的理論基礎(chǔ)是有窮狀態(tài)系統(tǒng)，狀態(tài)圖是后續(xù)模型檢驗中有限狀態(tài)機的基礎(chǔ)。構(gòu)建區(qū)間應(yīng)答器報文編制規(guī)則的UML狀態(tài)圖，如圖4所示。

圖4 報文編制規(guī)則的UML狀態(tài)轉(zhuǎn)移圖

其中列控數(shù)據(jù)類包含信號數(shù)據(jù)子類、應(yīng)答器位置表子類等；信息包內(nèi)容生成器類包含各類具體的信息包生成器子類。特性和事件的含義見表3。

4 報文編制規(guī)則的NuSMV建模與驗證

4.1 NuSMV模型

依照前文的方法，將擴展和抽象后的UML系統(tǒng)模型轉(zhuǎn)換為NuSMV模型，UML模型中每一個類對應(yīng)NuSMV模型的一個MODULE。以Q應(yīng)答器生成場景為例，以下為Main模塊和C1信息包內(nèi)容生成模塊對應(yīng)的NuSMV模型片段截取。

Main模塊片段與C1信息包內(nèi)容生成模塊：

MODULE main()

VAR // 聲明變量

BaliseInfo: boolean;

infoContentCreater: InfoContentCreater(…);

engDataTables: EngDataTables(…);

userDataPackets: UserDataPackets(…);

infoTypeConfirmer: InfoTypeConfirmer(…);

state: {Idle,BaliseTele_Created};

ASSIGN

init(BaliseInfo) := 0;

init(state):=Idle; // 定義初始狀態(tài)

next(state):= // 狀態(tài)轉(zhuǎn)移

case

state = Idle &(userDataPackets.UDP_Created=1): BaliseTele_Created;

TRUE : state;

esac;

SPEC AG (BaliseInfo=1 -> EF state_BaliseTele_Created) //待驗證的規(guī)范

?

C1信息包內(nèi)容生成模塊：

MODULE Info_C1(in_Con_C1, in_DataScope, in_Balise_is_Q_JZ, in_C1_LPACKET, in_E44_Created)

VAR

out_Create_C1: boolean;

out_Find_Q_JZ: boolean;

out_Create_E44: boolean;

?

state: {Idle, C1_Confirmed, Find_DataScope, DataScope_Confirmed, E44_Confirmed, C1_Created};

ASSIGN

init(out_Create_C1):= 0;

init(out_Find_Q_JZ):= 0;

init(out_Create_E44):= 0;

init(state):= Idle;

?

next(state):=

case

state = Idle & in_Con_C1=1 : C1_Confirmed;

state = C1_Confirmed & in_Balise_is_Q_JZ=1: Find_DataScope;

state = C1_Confirmed & in_Balise_is_Q_JZ=0: Find_DataScope;

state = Find_DataScope & in_DataScope=1: DataScope_Confirmed;

state = DataScope_Confirmed & in_C1_LPACKET=1: E44_Confirmed;

state = E44_Confirmed & in_E44_Created=1: C1_Created;

TRUE : state;

esac;

?

4.2 NuSMV模型的檢驗及結(jié)果分析

4.2.1 模型檢驗

對報文編制規(guī)則的NuSMV模型進行檢驗，由于模型待檢驗特性過多，因此本文僅對檢驗過程進行舉例介紹。

(1)活性驗證

例如表達式SPEC AG(EF(infoTypeConfirmer.state=InfoType_Confirmed))表示從任何狀態(tài)，經(jīng)過某些步驟可以確定用戶信息包種類。驗證結(jié)果為true。

(2)轉(zhuǎn)移性驗證

例如SPEC AG (state=Idle & EX(state= BaliseTele_Created))，表示報文編制結(jié)果能夠從狀態(tài)為空一步轉(zhuǎn)移到報文已生成狀態(tài)。驗證結(jié)果為true。

(3)反應(yīng)性驗證

例如表達式SPEC AG (infoContentCreater.info_C1.state= C1_Confirmed -> AF infoContentCreater.info_C1.out_Create_E44=1)的含義是：如果確定改組應(yīng)答器報文中含有C1包，則E44包一定已生成。驗證結(jié)果為true。

(4)互斥性

例如表達式SPEC !EF(infoContentCreater.in_BD=0 & infoContentCreater.info_C1.state= C1_Created)，表示找不到制動距離，則無法生成C1信息包。驗證結(jié)果為true。

(5)確定性驗證

例如表達SPEC !AG(infoTypeConfirmer.out_Con_E5=0 <-> infoContentCreater.info_E5.state= E5_Created)，表示確定沒有E5包和E5包的內(nèi)容已生成的兩個狀態(tài)一定不可以同時出現(xiàn)。驗證結(jié)果為true。

4.2.2 結(jié)果分析

如果某些系統(tǒng)性質(zhì)的驗證結(jié)果不是true，而是false，則需要根據(jù)NuSMV給出的反例對錯誤進行回溯追蹤、定位和修改，重新驗證修改后的模型。以下是由于文本語言描述應(yīng)答器應(yīng)用原則存在二義性導致在建模過程產(chǎn)生的反例，以此來說明反例結(jié)果分析的過程。

在深入分析挖掘應(yīng)答器應(yīng)用原則中描述的各信息包的內(nèi)容可以得出：區(qū)間應(yīng)答器報文應(yīng)滿足“如該區(qū)間應(yīng)答器組報文中生成了C1包，則該組報文一定已生成E44(C1)包”的特性。針對本條特性的模型檢驗的結(jié)果最初為false,驗證結(jié)果中反例提示為“沒有找到E44(C1)包已生成的狀態(tài)”。因此需對該反例進行分析，首先檢查系統(tǒng)NuSMV程序，確認沒有邏輯錯誤，符合UML模型的描述；再反向檢查UML模型，與區(qū)間應(yīng)答器組報文編制規(guī)則一致；再繼續(xù)追溯，發(fā)現(xiàn)在應(yīng)答器應(yīng)用原則中并未提及[ETCS-44]與CTCS包應(yīng)有的關(guān)系。最終錯誤定位在對于《CTCS-2級列控系統(tǒng)應(yīng)答器應(yīng)用原則》5.2.6.1節(jié) “每個[ETCS-44]包只能嵌入一個CTCS包”[1]這句規(guī)則的理解，應(yīng)在應(yīng)用原則中補充“每個CTCS包必須嵌入[ETCS-44]包才可作為完整的用戶信息包存在”，防止誤解。

4.2.3 模型檢驗的結(jié)論

對報文編制規(guī)則的NuSMV模型進行全面驗證，驗證結(jié)果均為true，表明所提取的應(yīng)答器報文編制規(guī)則滿足活性、轉(zhuǎn)移性、無死鎖性、確定性等要求。同時根據(jù)反例分析過程可以得到應(yīng)答器應(yīng)用原則存在的問題，即文本語言描述存在二義性。

5 結(jié)論

本文論述了應(yīng)答器報文數(shù)據(jù)以及其編制規(guī)則的重要性，指出《CTCS-2級列控系統(tǒng)應(yīng)答器應(yīng)用原則》[1]描述模糊，用文本語言描述存在二義性等問題，深度分析報文數(shù)據(jù)之間的關(guān)聯(lián)關(guān)系以及報文與列控數(shù)據(jù)之間的關(guān)聯(lián)關(guān)系，總結(jié)得到編制規(guī)則；采用UML與NuSMV相結(jié)合的方法對應(yīng)答器報文編制規(guī)則進行形式化建模與驗證，驗證了編制規(guī)則的轉(zhuǎn)移性、活性、反應(yīng)性等，最后在反例分析的過程中可以發(fā)現(xiàn)應(yīng)答器應(yīng)用原則存在的問題。驗證過程表明：

(1)UML與符號模型檢驗相結(jié)合的方法適用于應(yīng)答器報文編制規(guī)則的驗證。

(2)基于UML與符號模型檢驗相結(jié)合的形式化方法，能夠識別基于文本語言描述的應(yīng)答器應(yīng)用原則存在的二義性。

(3)通過對模型驗證的反例分析，可以建立正確且被唯一理解的應(yīng)用原則UML模型，用UML描述的應(yīng)用原則在實際應(yīng)用中可避免二義性問題，對于提高應(yīng)答器報文數(shù)據(jù)生成過程的正確性有重要意義。