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

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

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

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

1 系統(tǒng)建模元素定義

本文技術(shù)路線如圖1所示。基于需求規(guī)范，對系統(tǒng)建模元素進行定義，并結(jié)合模型架構(gòu)對系統(tǒng)的功能邏輯進行B模型的建模工作，通過定理證明和模型檢測兩種技術(shù)手段對建立的B模型進行形式化驗證，最終生成可執(zhí)行的C代碼。

圖1 技術(shù)路線Fig.1 Technical route

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

1.1 消息

PCS在運行過程中，不斷采集外部設(shè)備的信息，經(jīng)過一系列的邏輯判斷，最終產(chǎn)生新的驅(qū)動命令驅(qū)動外部設(shè)備改變狀態(tài)，以此來達到保證行車安全的目的。整理出這些消息有助于后續(xù)的建模工作。系統(tǒng)在循環(huán)工作中接收以及發(fā)送的部分消息如表1、2所示。

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

系統(tǒng)在每次循環(huán)工作中存在的內(nèi)部消息如表3所示。

表3 內(nèi)部消息Tab.3 Internal information

1.2 集合和常量

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

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

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

1.3 系統(tǒng)靜態(tài)數(shù)據(jù)關(guān)系

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

此外，還需注意，一條進路對應(yīng)的始端信號機只有一個，所以進路與信號機的數(shù)據(jù)關(guān)系可以用一維數(shù)組表示，如圖2所示。

圖2 進路與信號機的數(shù)據(jù)關(guān)系Fig.2 Data relationship between route and signal

進路與道岔、區(qū)段的關(guān)系比較復(fù)雜，一條進路會對應(yīng)多個道岔、多個區(qū)段，所以進路與道岔、區(qū)段的數(shù)據(jù)關(guān)系需要用二維數(shù)組來表示，如圖3所示。

圖3 進路與道岔、區(qū)段的數(shù)據(jù)關(guān)系Fig.3 Data relationship between route and point, as well route and section

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

2 系統(tǒng)功能B模型建立

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

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

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

2.1 系統(tǒng)體系結(jié)構(gòu)

系統(tǒng)完整的體系結(jié)構(gòu)如圖4所示（圖中省去了SEES靜態(tài)數(shù)據(jù)的內(nèi)容）。

圖4 系統(tǒng)體系結(jié)構(gòu)Fig.4 System architecture

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

2.2 機器文件PCS_Main

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

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

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

圖5 機器文件PCS_Main的部分內(nèi)容Fig.5 Partial “PCS_Main” representation

2.3 機器文件PCS_Main的實現(xiàn)

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

圖6 機器文件PCS_Main中操作Route_Operation的部分實現(xiàn)內(nèi)容Fig.6 Partial “Route_Operation” implementation in “PCS_Main”

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

2.4 機器文件PCS_Route

機器文件PCS_Route是PCS模型的主要部分，系統(tǒng)的主要運行邏輯都在該機器中被描述。除了描述人工控制道岔、信號機狀態(tài)的操作接口，還描述了進路控制過程的各個階段的操作接口。部分抽象變量如表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中描述的部分抽象操作更為復(fù)雜，如圖7所示操作中，用到ANY...WHERE...THEN...結(jié)構(gòu)，其目的是基于道岔、區(qū)段、信號機的任意選擇來描述一系列進路選排條件的檢查，之后執(zhí)行的變量Check_Condition_Result的賦值動作都依賴于此任意值。

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

3 系統(tǒng)屬性驗證及代碼生成

形式化語義符號描述了系統(tǒng)，更重要的是要對系統(tǒng)的性質(zhì)和安全性進行嚴(yán)格的證明，通過證明過程，揭示系統(tǒng)設(shè)計中的潛在缺陷。此外，將通過驗證后的B模型生成C代碼也是本節(jié)的目標(biāo)。

3.1 安全屬性驗證

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

現(xiàn)有安全屬性SRS-1：當(dāng)?shù)啦硖幱诮夥鉅顟B(tài)時，才可轉(zhuǎn)動道岔。將其轉(zhuǎn)換為不變式如公式（1）所示。

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

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

圖8 模型的證明情況統(tǒng)計Fig.8 Proof statistics of the model

3.2 代碼生成

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

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

4 總結(jié)

本文基于PCS的需求規(guī)范，整理出系統(tǒng)各模塊的建模元素，用形式的方式描述系統(tǒng)的非形式化的規(guī)范，使用形式化B方法以自頂向下的方式進行系統(tǒng)原型設(shè)計開發(fā)，將形式化方法應(yīng)用于系統(tǒng)需求分析至最終的代碼實現(xiàn)階段，得到以下主要結(jié)論。

1）對系統(tǒng)的功能邏輯建立形式化模型，實現(xiàn)對系統(tǒng)的需求規(guī)范、系統(tǒng)功能及決策過程的驗證，提高了系統(tǒng)模型的質(zhì)量。

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