鐵路信號(hào)聯(lián)鎖邏輯形式化建模研究

陳 良

（中鐵十九局集團(tuán)電務(wù)工程有限公司，北京 100076）

0 引言

在列車的通信系統(tǒng)中，計(jì)算機(jī)聯(lián)鎖系統(tǒng)是重要的設(shè)備之一。而隨著計(jì)算機(jī)聯(lián)鎖系統(tǒng)的不斷優(yōu)化迭代，其內(nèi)部系統(tǒng)構(gòu)造越來越精密、復(fù)雜。該系統(tǒng)不僅需要對(duì)邏輯的運(yùn)算，進(jìn)而控制信號(hào)機(jī)、道岔、站臺(tái)門、聯(lián)鎖進(jìn)路等裝置的聯(lián)動(dòng)控制，還需要與外部系統(tǒng)的信號(hào)進(jìn)行即時(shí)對(duì)接。在邏輯的運(yùn)算時(shí)還涉及了非常龐大的內(nèi)部狀態(tài)空間，而在與外部系統(tǒng)對(duì)接時(shí)通常會(huì)有大量的不確定性因素疊加，所以這類系統(tǒng)是一種非常精密、嚴(yán)苛的系統(tǒng)。有關(guān)資料顯示，形式化的研究對(duì)提高軟件質(zhì)量有著重大貢獻(xiàn)，其優(yōu)勢(shì)由此顯現(xiàn)。

1 鐵路信號(hào)與鐵路計(jì)算機(jī)信號(hào)系統(tǒng)的內(nèi)容

從鐵路交通角度來看，鐵路的信號(hào)是一個(gè)極其重要的領(lǐng)域。依據(jù)傳統(tǒng)方式可以對(duì)鐵路的信號(hào)進(jìn)行歸類劃分，當(dāng)列車的自動(dòng)控制系統(tǒng)應(yīng)用在城市軌道交通時(shí)，這種就是一個(gè)子域。近年來，在另外的3 種子系統(tǒng)中也不斷地開始應(yīng)用計(jì)算機(jī)技術(shù)。而利用計(jì)算機(jī)技術(shù)去解決鐵路信號(hào)領(lǐng)域中出現(xiàn)的問題，也是一種非常方便、實(shí)用的技術(shù)手段。在鐵路的計(jì)算機(jī)系統(tǒng)中，包含很多不同種類的子系統(tǒng)，而在一個(gè)調(diào)度區(qū)域內(nèi)，區(qū)間閉塞與車站聯(lián)鎖都是與列車運(yùn)行相關(guān)的部分。而在計(jì)算機(jī)信號(hào)系統(tǒng)中，色燈信號(hào)機(jī)、電動(dòng)轉(zhuǎn)轍機(jī)、軌道電路就是3 個(gè)室外的基礎(chǔ)設(shè)備，而對(duì)行車進(jìn)行指揮則是基礎(chǔ)設(shè)備必備條件。整個(gè)的列車運(yùn)行、停車都需要計(jì)算機(jī)的信號(hào)系統(tǒng)支持。系統(tǒng)控制層不僅是區(qū)間閉塞系統(tǒng)與車站聯(lián)鎖系統(tǒng)的核心，并且還是系統(tǒng)邏輯計(jì)算性能的實(shí)現(xiàn)者。

2 鐵路信號(hào)聯(lián)鎖邏輯形式化建模研究

2.1 形式化研究

2.1.1 通信的程序進(jìn)程

本質(zhì)上通信程序的進(jìn)程是根據(jù)進(jìn)程代數(shù)而演變的形式化方法，其主要使用于并發(fā)系統(tǒng)與分布式系統(tǒng)中。其基本原理是：對(duì)系統(tǒng)中的進(jìn)程交互，實(shí)現(xiàn)了描述與分析，并且形成了實(shí)體的數(shù)學(xué)框架。在進(jìn)程內(nèi)部中，可以實(shí)現(xiàn)信號(hào)的互相交互進(jìn)而產(chǎn)生關(guān)聯(lián)性影響，并且這種方法經(jīng)得起嚴(yán)密的數(shù)學(xué)邏輯考察。其主要運(yùn)作內(nèi)容是對(duì)進(jìn)程中出現(xiàn)的事件進(jìn)行細(xì)小的描述，并且進(jìn)程之間可以進(jìn)行運(yùn)算，然后與運(yùn)算結(jié)果進(jìn)行重合，進(jìn)而實(shí)現(xiàn)對(duì)復(fù)雜問題進(jìn)行詳細(xì)的描述。而運(yùn)算里包含并發(fā)進(jìn)程、選擇進(jìn)程、混合進(jìn)程等。而進(jìn)程的事件，如果發(fā)現(xiàn)相同事件可以交互，則把這種事件叫做通信事件。

2.1.2 B 方法的應(yīng)用

B 方法是種依據(jù)狀態(tài)的形式化方法，可以通過數(shù)理推算和邏輯運(yùn)算，從而建構(gòu)起數(shù)學(xué)理論的框架。其優(yōu)點(diǎn)在于可以建造軟件系統(tǒng)的特征與狀態(tài)，證明該框架的語法正確性，還能讓模型得到進(jìn)一步的精細(xì)化，從而讓抽象模型變得更加具體。抽象機(jī)是B方法中的基本構(gòu)成單位，抽象機(jī)的組成部分為變量、不變式、初始化、抽象機(jī)名等。

2.1.3 B 方法與通信程序進(jìn)程的有機(jī)結(jié)合

這兩種方法的結(jié)合，主要是考慮通信程序的進(jìn)程是以“事件驅(qū)動(dòng)”模式進(jìn)行驗(yàn)證的，只適合對(duì)單一空間的軟件系統(tǒng)進(jìn)行描述。而B 方法雖然不適合單一空間的軟件系統(tǒng)描述，但正因?yàn)槿绱?，才可以剛好彌補(bǔ)通信程序進(jìn)程這一缺點(diǎn)。對(duì)這兩種方法進(jìn)行互補(bǔ)式使用就一定可以滿足對(duì)復(fù)雜或單一空間的描述與分析。而它們連接的關(guān)鍵點(diǎn)在于，在開始兩種方法的操作之間建立起一個(gè)能夠?qū)崿F(xiàn)一對(duì)一的關(guān)系。只要能做到這兩種方法的同步，就可以做到對(duì)復(fù)雜、單一空間的監(jiān)控與管制。

2.1.4 有色PETRI 網(wǎng)的方法

有色PETRI 網(wǎng)（對(duì)離散并行系統(tǒng)的數(shù)學(xué)表示）分為分為層次有色PETRI 網(wǎng)與非層次有色PETRI 網(wǎng)兩種，前者即HCPN（基于分層有色PETRI），其中包括了很多的非層次的有色PETRI 網(wǎng)。而層次的PETRI 網(wǎng)是對(duì)多個(gè)的HCPN 模型進(jìn)行復(fù)合，使其的承載量變得更大。由此就能為非常復(fù)雜的空間提供分析與驗(yàn)證了，而這種方法的使用和高級(jí)程序開發(fā)語言所使用的層次。在HCPN 中，變遷方式為替代變遷與源變遷。而非層次的有色PETRI 網(wǎng)是理論基礎(chǔ)非常完善的形式化語言，但同時(shí)也有圖形結(jié)構(gòu)，是建模工具的一種。而有色PETRI 網(wǎng)還可以為許多的實(shí)踐應(yīng)用做建模起到非常重要的作用。在目前看來，對(duì)于有色PETRI 網(wǎng)的定義還存在一定的爭(zhēng)議。

2.1.5 TIMED SYNCCHARTS 建模方法

一般情況下，這種建模方式先要定義一個(gè)六元組，而SYNCCHARTS 是根據(jù)STATECHARTS 形式化的建模方式。但它并不具備時(shí)鐘約束，而且它的層次結(jié)構(gòu)太過簡(jiǎn)單，所以必須要定義好它的時(shí)間約束，并且還要做相關(guān)的宏布分析等計(jì)算工作。

2.2 鐵路信號(hào)聯(lián)鎖邏輯形式化建模

2.2.1 信號(hào)聯(lián)鎖的屬性特征

在鐵路中，車站信號(hào)聯(lián)鎖系統(tǒng)的主要作用是對(duì)行車安全進(jìn)行管控，該系統(tǒng)的功能主要有進(jìn)路空閑檢測(cè)技術(shù)、聯(lián)鎖技術(shù)、故障—安全技術(shù)等。而在車站的實(shí)際作業(yè)技術(shù)運(yùn)用中，被分為調(diào)車作業(yè)與列車作業(yè)。但無論是哪一種作業(yè)，都必須遵從從某一指定地點(diǎn)到另外一個(gè)指定地點(diǎn)運(yùn)行。而以列車為中心點(diǎn)，出發(fā)站與開入站和列車中心點(diǎn)的距離叫做進(jìn)路，所以在進(jìn)路中，必須先要保證列車調(diào)車作業(yè)的安全性。而想要達(dá)到這一效果，應(yīng)當(dāng)先要在進(jìn)路的入口位置放置防護(hù)信號(hào)機(jī)的設(shè)備。而按一般情況來看，鐵路的中線路較多，線路的兩端都連接著道岔，可以按照道岔的位置設(shè)置對(duì)應(yīng)的進(jìn)路。如果要檢測(cè)列車的進(jìn)路是否暢通，可以通過信號(hào)機(jī)的信號(hào)收發(fā)來查看。如果信號(hào)機(jī)顯示指示列車、車列進(jìn)入軌道，但道岔位置卻在另外一邊，就會(huì)產(chǎn)生交通事故。所以，為了保證行車安全，必須要保證充分使用信號(hào)機(jī)。最后，需要建立進(jìn)路，將進(jìn)路中的道岔轉(zhuǎn)變?yōu)檫M(jìn)路的指定位置，隨后開設(shè)防護(hù)信號(hào)機(jī)。如果道岔位置失誤，信號(hào)機(jī)的開放就會(huì)出現(xiàn)“失敗”的字樣。另外，在信號(hào)機(jī)的開設(shè)過程中，位于進(jìn)路中的道岔不可以被隨意變換位置。這就是道岔的聯(lián)鎖與信號(hào)機(jī)的關(guān)聯(lián)作用，而信號(hào)機(jī)對(duì)進(jìn)路與進(jìn)路、道岔與進(jìn)路等主體都存在關(guān)聯(lián)方關(guān)系。

2.2.2 開始鐵路信號(hào)聯(lián)鎖的建模

鐵路信號(hào)系統(tǒng)聯(lián)鎖復(fù)雜性，因?yàn)槠浔举|(zhì)上邏輯嚴(yán)密、復(fù)雜性強(qiáng)、車站作業(yè)種類等多種因素相關(guān)。如果規(guī)模比較小，作業(yè)形式單一，再加上車站周邊的地理結(jié)構(gòu)簡(jiǎn)單，那與之對(duì)應(yīng)的信號(hào)聯(lián)鎖系統(tǒng)就比較簡(jiǎn)單。但是，對(duì)像上海、北京這樣的大城市來說，其鐵路的信號(hào)聯(lián)鎖邏輯系統(tǒng)就非常復(fù)雜。而CBTC（Communication Based Train Control，基于通信的列車控制）的計(jì)算機(jī)聯(lián)鎖系統(tǒng)面向?qū)ο笫浅鞘熊壍澜煌ǎ梢酝ㄟ^計(jì)算機(jī)、信號(hào)機(jī)、通信等結(jié)合在一起，從而更好地實(shí)現(xiàn)對(duì)聯(lián)鎖進(jìn)路、信號(hào)機(jī)、站臺(tái)門等設(shè)備進(jìn)行動(dòng)態(tài)的監(jiān)控。讓通信接口與區(qū)域型的控制中心、列車自動(dòng)監(jiān)控系統(tǒng)、線路電子單元等外部系統(tǒng)進(jìn)行即時(shí)信息傳輸，從而一同完成列車運(yùn)行的控制，保障好列車的出行安全。而CBTC 聯(lián)鎖系統(tǒng)的邏輯運(yùn)算有非常復(fù)雜的空間，可以用B 方法進(jìn)行建模，其具體的步驟是聯(lián)鎖進(jìn)路控制、站場(chǎng)信號(hào)的平面圖等。其系統(tǒng)與外部系統(tǒng)連接因?yàn)榇嬖诜浅４蟮牟淮_定性，因此與外部系統(tǒng)連接的部分可以采用通信進(jìn)程來進(jìn)行建模。而關(guān)于B 方法對(duì)CBTC 聯(lián)鎖邏輯狀態(tài)的運(yùn)算，先要計(jì)算其核心，就是聯(lián)鎖進(jìn)路抽象機(jī)。由于其獨(dú)有的復(fù)雜性，所以可以采取分步精化。就是說，先建造一個(gè)初始狀態(tài)的聯(lián)鎖進(jìn)路的控制抽象機(jī)，然后再一點(diǎn)點(diǎn)添加相關(guān)的操作與狀態(tài)，讓它變得更加完善。在完成各類的抽象機(jī)計(jì)算之后，開始用通信進(jìn)程來建構(gòu)與外部交互的過程進(jìn)行計(jì)算。最后開始對(duì)CBTC 進(jìn)行分步精化。

第一步，添設(shè)緊急停車、站臺(tái)門等設(shè)備的狀態(tài)數(shù)據(jù)，并且補(bǔ)充這些狀態(tài)的數(shù)據(jù)，需要滿足其不變式的關(guān)系。按照進(jìn)路原則檢查，將這些數(shù)據(jù)填充到進(jìn)路操作部分。

第二步，與進(jìn)路的鎖閉過程結(jié)合，添加已開放區(qū)域、進(jìn)路的鎖閉狀態(tài)的數(shù)據(jù)，并給不變式做填充。

第三步，與進(jìn)路開放的過程結(jié)合，添設(shè)信號(hào)機(jī)的數(shù)據(jù)，并補(bǔ)充相關(guān)的不等式。

第四步，進(jìn)路的關(guān)閉，這里添加封閉信號(hào)機(jī)等的數(shù)據(jù)，繼續(xù)補(bǔ)充與之對(duì)應(yīng)的不等式關(guān)系。

最后一步就是與進(jìn)路的解鎖過程相結(jié)合，在開始解鎖進(jìn)路時(shí)，添加“三點(diǎn)檢查”等比較安全的解鎖邏輯規(guī)則。

對(duì)CBTC 的形態(tài)化驗(yàn)證，就是用原有的系統(tǒng)軟件檢測(cè)其是否可以滿足它的約束條件。而當(dāng)前比較多見的驗(yàn)證方法為模型檢驗(yàn)。但是計(jì)算機(jī)的聯(lián)鎖或可以采用層次有色PETRI 網(wǎng)來對(duì)復(fù)雜的空間進(jìn)行描述，而HCPN 模型就可以展開分層式的描述。因?yàn)閷哟斡猩玃ETRI 網(wǎng)具備完善的形式語言和圖形結(jié)構(gòu)，所以特別適合對(duì)計(jì)算機(jī)的聯(lián)鎖進(jìn)行描述，首先要根據(jù)其理論結(jié)構(gòu)基礎(chǔ)，對(duì)于各個(gè)層面上的聯(lián)鎖實(shí)體組建相對(duì)應(yīng)的HCPN 模型，組合后就可以形成一個(gè)完整的模型，而這時(shí)建立的模型才是聯(lián)鎖系統(tǒng)的HCPN 模型。而在鐵路信號(hào)系統(tǒng)中，不僅有聯(lián)鎖關(guān)系，還有其他的運(yùn)行規(guī)律。其建模的主要目的在于以更精確地形式化使聯(lián)鎖設(shè)備變得更容易控制，所以，同樣也可以把車站信號(hào)的聯(lián)鎖分層、分類，這樣才能更好地對(duì)聯(lián)鎖系統(tǒng)進(jìn)行“分解”。

3 結(jié)束語

在鐵路號(hào)聯(lián)鎖邏輯中，對(duì)于形式化的建模研究，可以采取多種多樣的方式進(jìn)行建模。本文簡(jiǎn)單探討了B 方法與通信進(jìn)程的結(jié)合使用，介紹了CBTC 計(jì)算機(jī)信號(hào)系統(tǒng)的建模。隨著城市交通軌道的大力發(fā)展，計(jì)算機(jī)式的聯(lián)鎖系統(tǒng)模式必將引領(lǐng)新的交通系統(tǒng)技術(shù)，而傳統(tǒng)的電聯(lián)式的聯(lián)鎖必將逐步“退役”。只有交通系統(tǒng)大量迭代新穎的技術(shù)、高端的技術(shù)才能為人們出行帶來實(shí)惠，才能提供更好的交通質(zhì)量、速度、安全服務(wù)。另外，鐵路交通系統(tǒng)不僅會(huì)因?yàn)楦鼡Q高新技術(shù)而帶來更加穩(wěn)定、更令人滿意的體驗(yàn)，還可以更好地占領(lǐng)市場(chǎng)，為地鐵、鐵路的運(yùn)營(yíng)帶來實(shí)實(shí)在在的利潤(rùn)。