應答器報文編制規則的形式化建模與驗證

黃 旭，劉中田

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

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

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

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

1 應答器報文編制規則的提取

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

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

圖1 應答器報文編制規則的整理方法

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

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

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

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

表1 應答器報文編制規則示例

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

(1)規則管理階段

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

(2)建模階段

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

(3)模型驗證階段

模型檢驗工具NuSMV遍歷搜索輸入的有窮狀態系統模型，檢驗系統模型是否滿足指定的性質。

(4)模型檢驗結果分析

若系統不滿足指定的性質，則根據反例驗證結果對錯誤進行回溯、定位、修改和重新驗證。

2.1 面向NuSMV的UML建模

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

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

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

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

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

2.2 NuSMV建模

將2.1節中擴展和抽象后的UML模型轉換為NuSMV模型，轉換規則如下：

(1)NuSMV系統結構

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

(2)MODULE部分

UML模型中每個類的輸入事件對應相應MODULE的形式化參數，并且在每個輸入事件前加前綴“in_”作為模塊輸入參數名，作用是使子模塊與主模塊關聯。

(3)VAR部分

變量聲明使用關鍵字VAR，主要用來創建組件關系、聲明模塊狀態機狀態和類的屬性。每個類的屬性轉換為對應MODULE的VAR下的變量；每個屬性的數據類型轉換為對應變量的數據類型；狀態機的狀態應在VAR部分聲明。

(4)ASSIGN部分

變量賦值使用AGGGN關鍵字，主要用來說明狀態和屬性的初始變化以及變化機制。

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

2.3 NuSMV模型檢驗及結果分析

2.3.1 模型檢驗

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

(1)活性驗證

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

(2)轉移性驗證

轉移性是指系統在狀態s1和狀態s2間可以互相轉移。對應驗證的CTL公式為：EF(state=s1 & EX(state=s2))。

(3)反應性驗證

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

CTL算子“->”關系真值表見表2。

(4)互斥性

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

(5)確定性驗證

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

2.3.2 反例分析

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

3 報文編制規則的UML建模

針對報文編制規則的管理結果，本文以Q應答器報文的生成場景為例，建立應答器報文編制規則的UML類圖、時序圖和狀態圖。

3.1 UML類圖

采用面向對象的方法將編制規則抽象為4個相互關聯的類，分別是信息包種類確定器類InfoTypeConfirmer、信息包內容生成器類InfoContentCreater、列控數據類EngDataTables和用戶報文類UserDataPackets，其中信息包內容生成器類包含了Head、E5、C1…等生成子類。圖3所示為擴展和抽象后的UML類圖，每個類都有其對應的接收信息和輸出操作，接收信息以?signal?開頭，輸出操作以“+”開頭。例如InfoTypeConfirmer的接收信息有BaliseInfo()，輸出的操作是Con_E5()、Con_C1()等，具體字段含義見表3。

圖3 報文編制規則的UML類圖

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

3.2 UML狀態轉移圖

狀態圖主要用來描述對象、子系統、系統的生命周期，模型檢驗的理論基礎是有窮狀態系統，狀態圖是后續模型檢驗中有限狀態機的基礎。構建區間應答器報文編制規則的UML狀態圖，如圖4所示。

圖4 報文編制規則的UML狀態轉移圖

其中列控數據類包含信號數據子類、應答器位置表子類等；信息包內容生成器類包含各類具體的信息包生成器子類。特性和事件的含義見表3。

4 報文編制規則的NuSMV建模與驗證

4.1 NuSMV模型

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

Main模塊片段與C1信息包內容生成模塊：

MODULE main()

VAR // 聲明變量

BaliseInfo: boolean;

infoContentCreater: InfoContentCreater(…);

engDataTables: EngDataTables(…);

userDataPackets: UserDataPackets(…);

infoTypeConfirmer: InfoTypeConfirmer(…);

state: {Idle,BaliseTele_Created};

ASSIGN

init(BaliseInfo) := 0;

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

next(state):= // 狀態轉移

case

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

TRUE : state;

esac;

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

?

C1信息包內容生成模塊：

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模型的檢驗及結果分析

4.2.1 模型檢驗

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

(1)活性驗證

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

(2)轉移性驗證

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

(3)反應性驗證

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

(4)互斥性

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

(5)確定性驗證

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

4.2.2 結果分析

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

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

4.2.3 模型檢驗的結論

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

5 結論

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

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

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

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