列車通信網(wǎng)絡(luò)系統(tǒng)形式化建模與驗(yàn)證方法研究

朱小艷+廉雪瑩+趙云婷

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

關(guān)鍵詞：列車通信網(wǎng)絡(luò)；形式化建模；靜態(tài)屬性分析；形式化驗(yàn)證；模擬驗(yàn)證

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

一、列車通信網(wǎng)絡(luò)系統(tǒng)的形式化建模概述

（一）UML

UML是Unified Modeling Language的英文縮寫(xiě)，又稱為統(tǒng)一建模語(yǔ)言。UML是二十世紀(jì)末期由對(duì)象管理組織發(fā)布的一種建模語(yǔ)言，其具備定義良好、功能強(qiáng)大以及使用便捷等諸多優(yōu)點(diǎn)，因而在業(yè)界得到了廣泛使用[1]。UML支持對(duì)軟件密集系統(tǒng)的可視化建模，并且具有面向?qū)ο笳Z(yǔ)言的特征，即其理念是“讓語(yǔ)言適應(yīng)問(wèn)題，而不是要問(wèn)題適應(yīng)語(yǔ)言”，它能夠讓開(kāi)發(fā)人員關(guān)注與系統(tǒng)的模型和結(jié)構(gòu)，而不是系統(tǒng)實(shí)現(xiàn)的具體細(xì)節(jié)，適用于數(shù)據(jù)建模、業(yè)務(wù)建模、對(duì)象建模以及組件建模等。

（二）Petri網(wǎng)

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

Petri網(wǎng)理論經(jīng)過(guò)業(yè)界多年的實(shí)踐與完善，目前已經(jīng)形成多層次、多分支的理論結(jié)構(gòu)，從其外延上可以分為基本Petri網(wǎng)、有色Petri網(wǎng)、增廣Petri網(wǎng)以及含時(shí)間因素的Petri網(wǎng)等，其中有色Petri網(wǎng)、增廣Petri網(wǎng)以及含時(shí)間因素的Petri網(wǎng)均可以稱作高級(jí)Petri網(wǎng)。高級(jí)Petri網(wǎng)是對(duì)基本Petri網(wǎng)的擴(kuò)展和抽象，其能夠做到對(duì)網(wǎng)中的托肯進(jìn)行分類、解析和運(yùn)算，減少網(wǎng)系統(tǒng)中國(guó)的基本元素，以便實(shí)現(xiàn)縮小網(wǎng)系統(tǒng)規(guī)模的目標(biāo)[3]。高級(jí)Petri網(wǎng)的主要優(yōu)勢(shì)是當(dāng)其對(duì)復(fù)雜的系統(tǒng)進(jìn)行建模時(shí)，所建立的模型將更為簡(jiǎn)單、清晰以及直觀。

（三）時(shí)間自動(dòng)機(jī)

時(shí)間自動(dòng)機(jī)是一種用于實(shí)時(shí)系統(tǒng)建模和驗(yàn)證的理論，其以基本有限自動(dòng)機(jī)的為基礎(chǔ)，并加入了實(shí)時(shí)變量建模時(shí)鐘集合，時(shí)鐘變量的限制用于控制自動(dòng)機(jī)的行為，相關(guān)研究機(jī)構(gòu)在其理論技術(shù)上開(kāi)發(fā)了時(shí)間自動(dòng)機(jī)屬性驗(yàn)證工具，比如UPPAAL以及Kronos等，實(shí)現(xiàn)了自動(dòng)化驗(yàn)證過(guò)程的高效執(zhí)行。

二、列車通信網(wǎng)絡(luò)系統(tǒng)的形式化驗(yàn)證方法

形式化驗(yàn)證過(guò)程如圖2所示，較其他驗(yàn)證方法，其具備四大優(yōu)勢(shì)：第一，驗(yàn)證情況蘊(yùn)含所有的激勵(lì)空間，驗(yàn)證過(guò)程和理論是完整的；第二，驗(yàn)證結(jié)果的正確性以數(shù)學(xué)理論為保障，與系統(tǒng)的激勵(lì)情況無(wú)關(guān)；第三，驗(yàn)證結(jié)果不需要建立參考模型，生成期望的輸出序列；第四，當(dāng)驗(yàn)證發(fā)現(xiàn)錯(cuò)誤時(shí)，可以生成簡(jiǎn)單易懂的錯(cuò)誤調(diào)試信息[4]。當(dāng)前，形式化驗(yàn)證方法主要包括定理證明、模型檢查以及等價(jià)性檢查。

（一）定理證明

定理證明（Theorem Proving）的目標(biāo)是借助公理和推理規(guī)則等形式化邏輯證明設(shè)計(jì)的正確性。在理論證明系統(tǒng)中，通過(guò)邏輯架構(gòu)對(duì)設(shè)計(jì)進(jìn)行描述，并用引理對(duì)一系列性質(zhì)進(jìn)行描述，引理需要通過(guò)一些推理規(guī)則證明正確性。一級(jí)邏輯和高級(jí)邏輯能夠準(zhǔn)確無(wú)誤地實(shí)現(xiàn)系統(tǒng)信息的表達(dá)，進(jìn)而有效規(guī)避了自然語(yǔ)言描述系統(tǒng)帶來(lái)的不準(zhǔn)確的風(fēng)險(xiǎn)。

定理證明系統(tǒng)可以處理復(fù)雜的邏輯運(yùn)算，定理證明過(guò)程以公理、推理規(guī)則、中間引理以及派生定義為依托，一般而言，往往需要具有專業(yè)素養(yǎng)過(guò)硬的人員進(jìn)行推理路線的選定，進(jìn)而交互式的完成證明過(guò)程。

（二）模型檢查

上世紀(jì)末期E.M.Clarke等提出了基于師太邏輯和有限狀態(tài)轉(zhuǎn)移圖的模型檢查方法之后，模型檢查方法因?yàn)檩^定理證明方法具有更高的自動(dòng)化程度的優(yōu)勢(shì)，而在世界上各個(gè)研究機(jī)構(gòu)和實(shí)驗(yàn)室得到深入研究和普及應(yīng)用，以后經(jīng)過(guò)了許多年的實(shí)踐和完善。模型檢查方法以時(shí)態(tài)邏輯為基本思想，描述程序或電路的時(shí)序性質(zhì)，使用Kripke結(jié)構(gòu)表示程序或電路的行為和結(jié)構(gòu)，通過(guò)Kripke結(jié)構(gòu)驗(yàn)證其是否滿足時(shí)態(tài)邏輯公式。

結(jié)語(yǔ)

綜上所述，我國(guó)幅員遼闊、人員眾多的基本國(guó)情決定了構(gòu)建安全可靠、經(jīng)濟(jì)環(huán)保以及實(shí)用快捷的高速列車的重要意義。盡管高速列車網(wǎng)絡(luò)系統(tǒng)仍存在一些問(wèn)題，但是隨著高速列車網(wǎng)絡(luò)系統(tǒng)形式化建模和驗(yàn)證方法的實(shí)踐和不斷完善，我國(guó)的高速列車客運(yùn)業(yè)到一定可以實(shí)現(xiàn)更為良好的發(fā)展。

參考文獻(xiàn)：

[1] 孫立宏，洪一.？？基于VMM統(tǒng)一驗(yàn)證平臺(tái)的處理器芯片功能驗(yàn)證[J]. 火控雷達(dá)技術(shù). 2010（01）

[2] 陳江，陳建國(guó)，陸慧娟，王康健.？？UML時(shí)間順序圖的實(shí)時(shí)系統(tǒng)建模及驗(yàn)證[J]. 中國(guó)計(jì)量學(xué)院學(xué)報(bào). 2010（01）

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

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