基于B方法的道岔控制系統形式化建模與驗證

劉 寧，韓 程，王 崢，侯錫立，王恪銘

（1．西南交通大學唐山研究生院，河北唐山 063000；2．北京全路通信信號研究設計院集團有限公司，北京 100070；3．通號粵港澳（廣州）交通科技有限公司，廣州，511400；4．西南交通大學系統可信性自動驗證國家地方聯合工程實驗室，成都 610031）

形式化方法是描述系統性質的基于數學的技術，指一類有嚴格數學語義的方法，它提供了一個可以在其中以系統的方式描述、開發、驗證系統的框架[1]。人們使用具有精確語義的符號描述所要設計的軟件系統，并對所描述的系統進行嚴格證明，可以揭示設計中的缺陷。通過使用形式化方法開發、驗證系統，可以很大程度減少設計缺陷，提高系統的安全性[2]。

道岔控制系統（Point Control System，PCS）作為城市輕型軌道交通信號控制系統中分布式聯鎖子系統使用。目前已有大量學者將形式化方法運用在聯鎖系統的開發過程中[3-8]。以上研究針對系統的功能安全進行研究，盡可能減少系統設計缺陷，集中在系統需求分析階段，而對形式化方法在系統需求分析階段到代碼實現階段的應用研究不足，且缺少運用形式化方法開發PCS的研究。本文針對以上不足之處，嘗試使用形式化B方法開發PCS，將系統建模、驗證及編碼等工作進行融合，推廣形式化方法在國內的應用。

1 系統建模元素定義

本文技術路線如圖1所示?；谛枨笠幏?，對系統建模元素進行定義，并結合模型架構對系統的功能邏輯進行B模型的建模工作，通過定理證明和模型檢測兩種技術手段對建立的B模型進行形式化驗證，最終生成可執行的C代碼。

圖1 技術路線Fig.1 Technical route

為使非形式化的需求規范信息變得精確，用形式化的方式去描述該系統的非形式化規范，需明確系統的輸入/輸出消息以及各個消息可能取到的值等信息。本節通過定義變量、常量、靜態數據及其關系描繪出系統的大致框架，便于后續的建模工作。

1.1 消息

PCS在運行過程中，不斷采集外部設備的信息，經過一系列的邏輯判斷，最終產生新的驅動命令驅動外部設備改變狀態，以此來達到保證行車安全的目的。整理出這些消息有助于后續的建模工作。系統在循環工作中接收以及發送的部分消息如表1、2所示。

表1 部分輸入消息Tab.1 Partial input information

系統在每次循環工作中存在的內部消息如表3所示。

表3 內部消息Tab.3 Internal information

1.2 集合和常量

本節定義在形式化建模階段需要的靜態數據，思想是將同一類狀態歸為一個集合。此外，靜態數據還應包括一些表示命令的常量。下面定義一些單獨的表示命令的常量，主要是一些命令表示信息，方便后續建模時使用，如表4所示。

表2 部分輸出消息Tab.2 Partial output information

表4 表示命令的部分常量Tab.4 Partial constants for indication commands

1.3 系統靜態數據關系

為了在建模時便于描述聯鎖表的各種數據，采用最簡單、直接的方式，即將進路數據提前定義。對所有進路、信號機、道岔、區段從0開始進行編號，將其當作靜態數據，放在單獨一個抽象機中，方便其他模塊在需要進路信息時參考。

此外，還需注意，一條進路對應的始端信號機只有一個，所以進路與信號機的數據關系可以用一維數組表示，如圖2所示。

圖2 進路與信號機的數據關系Fig.2 Data relationship between route and signal

進路與道岔、區段的關系比較復雜，一條進路會對應多個道岔、多個區段，所以進路與道岔、區段的數據關系需要用二維數組來表示，如圖3所示。

圖3 進路與道岔、區段的數據關系Fig.3 Data relationship between route and point, as well route and section

但還需注意，每條進路所包含的道岔數量也存在不相等的情況。為表示某條進路是否跟某個信號機、區段有關系，還需單獨定義一個數據關系來表示，即判斷進路與道岔、區段編號之間的關系是否為TRUE，若是，則說明該編號的道岔（區段）與該條進路有關聯；若否，則說明該編號的道岔（區段）與該條進路無關聯。

2 系統功能B模型建立

B方法作為軟件開發方法，最初由J-R Abrial在1980年提出，其基本思想是提供一種表示方法，使用“抽象機記法”和“廣義代換語言”來描述軟件[9]，用它描述的軟件最終可以用過程性的高級語言實現，甚至是匯編語言。該方法提供一個框架，在該框架中可以完善規范直至實現，可以將實現轉換為C編程語言。B方法是第一個單一的形式化方法，涵蓋了從規范到設計到實現的軟件開發過程的所有階段。

B方法的基礎是集合論、關系代數和一階謂詞邏輯，他們都有嚴格的形式和精確的定義。使用B方法描述軟件的基本單元是抽象機，該抽象機包括：數據描述（常量、變量）；操作描述（數據上的一組操作）；不變式（數據狀態必須滿足的一組關系）。

將對應道岔控制系統的規范描述和設計給出其形式化模型。從外界需要的系統接口，即外部操作人員需要的功能開始，建立一個非常抽象、不確定的系統規范模型，然后逐步精化，引入描述細節，由最開始的描述“做什么”到最終的描述“怎么做”。為便于描述，下面展示的形式化B模型是簡化后的版本，該B模型基于單條線路建立，線路只涉及單個信號機、單個道岔、單個區段。

2.1 系統體系結構

系統完整的體系結構如圖4所示（圖中省去了SEES靜態數據的內容）。

圖4 系統體系結構Fig.4 System architecture

系統的體系結構，即模型框架，需要在建模前確定。因為要考慮到模塊消息的交互，若模型框架不合適，模塊之間無法有效的將信息交互，同時給后續的形式化驗證工作帶來不便。

2.2 機器文件PCS_Main

在該機器中描述了一些帶有輸入參數的操作，通過該機器提供的接口，外部工作人員就能夠進行一些基本操作。這些操作不需要描述細節，只負責給外部提供一個接口，所有代換都用“skip”代替。機器文件PCS_Main包含的部分操作如表5所示。

表5 機器文件PCS_Main包含的部分操作Tab.5 Partial operations contained in “PCS_Main”

該機器中的操作示例如圖5所示。在考慮該機器的抽象操作時，只描述了一個非常不確定的輪廓，甚至沒有不變式，即這些抽象操作沒有要維持的不變式，故該機器不會產生證明義務。

圖5 機器文件PCS_Main的部分內容Fig.5 Partial “PCS_Main” representation

2.3 機器文件PCS_Main的實現

區別于分解操作的實現方式，基于機器文件PCS_Route和機器文件PCS_Input實現機器文件PCS_Main的基本想法是利用機器文件PCS_Input中一些查詢操作的輸出信息和機器文件PCS_Route中的部分操作來實現機器文件PCS_Main中的相應操作，如圖6所示。

圖6 機器文件PCS_Main中操作Route_Operation的部分實現內容Fig.6 Partial “Route_Operation” implementation in “PCS_Main”

顯然，該操作的實現相比于規范描述顯得很復雜，不但用到被導入抽象機的操作，還用到VAR…IN…結構，IF結構嵌套。該操作描述了進路控制過程，包括進路選排、進路鎖閉、信號開放與信號保持以及進路解鎖。具體過程：進行進路操作時，先調用操作UPDATE_ROUTE_CONDITION_FUN和操作CHECK_POINT_POS，用來判斷進路選排條件是否滿足，其中操作UPDATE_ROUTE_CONDITION_FUN和操作CHECK_POINT_POS的保衛條件與執行語句根據相應需求文檔得到。若進路選排條件滿足，則執行進路選排操作，并且再次調用上述兩個操作，判斷進路鎖閉條件是否滿足。如果進路鎖閉條件滿足，則執行進路鎖閉操作，同時調用操作SIGNAL_FILAMENT_QU判斷信號開放條件是否滿足。若信號開放條件滿足，則進行信號開放，并且調用操作SECTION_STATUS_QUERY_FUN判斷進路上區段的狀態信息，即進路解鎖的檢查條件。若滿足此條件，則執行進路解鎖操作。

2.4 機器文件PCS_Route

機器文件PCS_Route是PCS模型的主要部分，系統的主要運行邏輯都在該機器中被描述。除了描述人工控制道岔、信號機狀態的操作接口，還描述了進路控制過程的各個階段的操作接口。部分抽象變量如表6所示。

表6 機器文件PCS_Route中定義的部分抽象變量Tab.6 Partial abstract variables defined in “PCS_Route”

該機器文件中包含的部分操作如表7所示。

表7 機器文件PCS_Route中定義的部分操作Tab.7 Partial operations defined in “PCS_Route”

相較于機器文件PCS_Main描述的抽象操作，機器文件PCS_Route中描述的部分抽象操作更為復雜，如圖7所示操作中，用到ANY...WHERE...THEN...結構，其目的是基于道岔、區段、信號機的任意選擇來描述一系列進路選排條件的檢查，之后執行的變量Check_Condition_Result的賦值動作都依賴于此任意值。

圖7 操作UPDATE_ROUTE_CONDITION_FUN的代碼Fig.7 Code of operating “UPDATE_ROUTE_CONDITION_FUN”

3 系統屬性驗證及代碼生成

形式化語義符號描述了系統，更重要的是要對系統的性質和安全性進行嚴格的證明，通過證明過程，揭示系統設計中的潛在缺陷。此外，將通過驗證后的B模型生成C代碼也是本節的目標。

3.1 安全屬性驗證

本小節主要圍繞形式化驗證展開，即通過將系統的安全屬性描述為不變式（invariant），以此來約束系統的常量、變量之間的關系，保證系統狀態的改變都是在規定的范圍內，從而確保系統運行過程的安全性。

現有安全屬性SRS-1：當道岔處于解封狀態時，才可轉動道岔。將其轉換為不變式如公式（1）所示。

此時該不變式產生的關于操作POINT_ROUTE_UNBLOCK_FUN的證明義務未通過。原因是操作POINT_ROUTE_UNBLOCK_FUN的代換語句中會改變Point_Block_State的值，故需要證明在該變量值改變后仍然能夠維持不變式所描述的靜態規則。在操作POINT_ROUTE_UNBLOCK_FUN中添加一個前條件Point Pos : {PCS_POINT_NORMAL,PCS_POINT_REVERSE}，上述證明義務成立。

上述模型共計生成154條證明義務，通過完善模型中的形式表達，以及結合手動交互式證明策略，最后所有生成的證明義務都證明通過。證明義務統計情況如圖8所示。

圖8 模型的證明情況統計Fig.8 Proof statistics of the model

3.2 代碼生成

Atelier B支持將形式化B模型轉換為高級編程語言，使得形式化B方法貫通軟件系統開發的全過程。排列某條進路的場景如圖9所示，當進路排列后，信號機燈絲工作正常，則可以開放信號機；但在執行解鎖進路時，輸入區段被占用的信息，則進路無法解鎖。C代碼的運行結果滿足此需求。

圖9 代碼運行情況示例Fig.9 Demonstration of code running

4 總結

本文基于PCS的需求規范，整理出系統各模塊的建模元素，用形式的方式描述系統的非形式化的規范，使用形式化B方法以自頂向下的方式進行系統原型設計開發，將形式化方法應用于系統需求分析至最終的代碼實現階段，得到以下主要結論。

1）對系統的功能邏輯建立形式化模型，實現對系統的需求規范、系統功能及決策過程的驗證，提高了系統模型的質量。

2）通過這種開發方式，將驗證后的系統模型生成可執行代碼，減少了編碼階段的工作量，間接減少測試反饋修改的工作量。