列車通信網絡系統形式化建模與驗證方法研究

朱小艷+廉雪瑩+趙云婷

摘要：隨著現場總線技術、計算機網絡通信技術、嵌入式系統控制技術以及故障診斷技術的高速發展，當前列車控制系統已經實現了從孤立的數字控制系統向基于網絡的分布式控制系統的轉變。在現下我國高速鐵路迅猛發展的浪潮下，列車通信網絡系統的自主研發、設備制造以及維護運營等課題引起了各大高校和研究機構的高度重視。然而，在列車客運業碩果累累的同時，其諸多問題在系統設計過程中變得日漸凸顯。本文對基于形式化方法和模擬方法的列車系統建模及驗證的相關研究進行了重點探討。

關鍵詞：列車通信網絡；形式化建模；靜態屬性分析；形式化驗證；模擬驗證

我國幅員遼闊、人員眾多的基本國情決定了構建安全可靠、經濟環保以及實用快捷的高速列車的重要意義。隨著二十一世紀初葉我國第一條高速鐵路京津城際高鐵的正式通車運營，我國從此邁入了高速列車時代。根據《中國鐵路中長期規劃》，二零二零年我國將建設二百公里時速以上的高速鐵路長達約兩萬公里，以便滿足人民群眾日益增長的出行需要。隨著列車通信網絡的逐漸發展和創新升級，其取得了不菲的成就，然而在自主研發、設備制造以及維護運營等相關問題上尚未有切實可行的方案。但是我國鐵路尚還處于起步階段，迫切需要高速列車關鍵技術的技術支持。

一、列車通信網絡系統的形式化建模概述

（一）UML

UML是Unified Modeling Language的英文縮寫，又稱為統一建模語言。UML是二十世紀末期由對象管理組織發布的一種建模語言，其具備定義良好、功能強大以及使用便捷等諸多優點，因而在業界得到了廣泛使用[1]。UML支持對軟件密集系統的可視化建模，并且具有面向對象語言的特征，即其理念是“讓語言適應問題，而不是要問題適應語言”，它能夠讓開發人員關注與系統的模型和結構，而不是系統實現的具體細節，適用于數據建模、業務建模、對象建模以及組件建模等。

（二）Petri網

Petri網是德國科學家Carl Adam Petri博士于二十世紀中葉在其博士論文《Kommunikationmit Automaten》中首次提出的，然后經過了長達40余年的發展和完善，逐步形成的一種完整、系統的通用建模語言[2]。Petri網不僅可以勾勒系統的結構，還能描述系統的動態行為，當前其在計算機科學與技術、自動化科學技術、機械設計與制造、工業過程控制以及經濟學等領域都得到了普及應用。Petri網是一種基于圖形的數學建模語言，其既可以通過圖形界面模擬系統的行為特征，又能夠結合線性代數、矩陣論等相關數學理論對系統的性質進行有效的分析，Petri網的分類如圖1所示。

Petri網理論經過業界多年的實踐與完善，目前已經形成多層次、多分支的理論結構，從其外延上可以分為基本Petri網、有色Petri網、增廣Petri網以及含時間因素的Petri網等，其中有色Petri網、增廣Petri網以及含時間因素的Petri網均可以稱作高級Petri網。高級Petri網是對基本Petri網的擴展和抽象，其能夠做到對網中的托肯進行分類、解析和運算，減少網系統中國的基本元素，以便實現縮小網系統規模的目標[3]。高級Petri網的主要優勢是當其對復雜的系統進行建模時，所建立的模型將更為簡單、清晰以及直觀。

（三）時間自動機

時間自動機是一種用于實時系統建模和驗證的理論，其以基本有限自動機的為基礎，并加入了實時變量建模時鐘集合，時鐘變量的限制用于控制自動機的行為，相關研究機構在其理論技術上開發了時間自動機屬性驗證工具，比如UPPAAL以及Kronos等，實現了自動化驗證過程的高效執行。

二、列車通信網絡系統的形式化驗證方法

形式化驗證過程如圖2所示，較其他驗證方法，其具備四大優勢：第一，驗證情況蘊含所有的激勵空間，驗證過程和理論是完整的；第二，驗證結果的正確性以數學理論為保障，與系統的激勵情況無關；第三，驗證結果不需要建立參考模型，生成期望的輸出序列；第四，當驗證發現錯誤時，可以生成簡單易懂的錯誤調試信息[4]。當前，形式化驗證方法主要包括定理證明、模型檢查以及等價性檢查。

（一）定理證明

定理證明（Theorem Proving）的目標是借助公理和推理規則等形式化邏輯證明設計的正確性。在理論證明系統中，通過邏輯架構對設計進行描述，并用引理對一系列性質進行描述，引理需要通過一些推理規則證明正確性。一級邏輯和高級邏輯能夠準確無誤地實現系統信息的表達，進而有效規避了自然語言描述系統帶來的不準確的風險。

定理證明系統可以處理復雜的邏輯運算，定理證明過程以公理、推理規則、中間引理以及派生定義為依托，一般而言，往往需要具有專業素養過硬的人員進行推理路線的選定，進而交互式的完成證明過程。

（二）模型檢查

上世紀末期E.M.Clarke等提出了基于師太邏輯和有限狀態轉移圖的模型檢查方法之后，模型檢查方法因為較定理證明方法具有更高的自動化程度的優勢，而在世界上各個研究機構和實驗室得到深入研究和普及應用，以后經過了許多年的實踐和完善。模型檢查方法以時態邏輯為基本思想，描述程序或電路的時序性質，使用Kripke結構表示程序或電路的行為和結構，通過Kripke結構驗證其是否滿足時態邏輯公式。

結語

綜上所述，我國幅員遼闊、人員眾多的基本國情決定了構建安全可靠、經濟環保以及實用快捷的高速列車的重要意義。盡管高速列車網絡系統仍存在一些問題，但是隨著高速列車網絡系統形式化建模和驗證方法的實踐和不斷完善，我國的高速列車客運業到一定可以實現更為良好的發展。

參考文獻：

[1] 孫立宏，洪一.？？基于VMM統一驗證平臺的處理器芯片功能驗證[J]. 火控雷達技術. 2010（01）

[2] 陳江，陳建國，陸慧娟，王康健.？？UML時間順序圖的實時系統建模及驗證[J]. 中國計量學院學報. 2010（01）

[3] 傅游，花嶸，田銀花.？？基于帶抑制弧的Petri網的min-min算法模型研究[J]. 計算機應用研究. 2010（01）

朱小艷，1985年10月28日出生，性別女，民族漢，籍貫安徽池州，單位中車南京浦鎮車輛有限公司，郵編210032，職稱助理工程師，學歷碩士，研究方向列車通信網絡