陶 玲，宋 軍

基于CPN的聯(lián)鎖系統(tǒng)選岔網(wǎng)絡(luò)建模及驗(yàn)證

陶 玲，宋 軍

在詳細(xì)分析聯(lián)鎖系統(tǒng)選岔電路的前提下，抽象出選岔網(wǎng)絡(luò)的聯(lián)鎖邏輯條件，并采用有色Petri網(wǎng)（Colored Petri Net，CPN）為其建立形式化驗(yàn)證模型，同時(shí)采用CPN TOOLS對(duì)所建立的模型進(jìn)行仿真及狀態(tài)空間分析，結(jié)果表明所建立的模型能夠很好的描述選岔網(wǎng)絡(luò)的工作狀態(tài)。

選岔網(wǎng)絡(luò)；CPN；形式化；CPN TOOLS

0 引言

鐵路信號(hào)計(jì)算機(jī)聯(lián)鎖軟件是鐵路信號(hào)系統(tǒng)中非常重要的安全苛求軟件，對(duì)保障行車安全至關(guān)重要，而針對(duì)聯(lián)鎖軟件中聯(lián)鎖邏輯關(guān)系形式化驗(yàn)證方法的研究將有利于減少聯(lián)鎖軟件開發(fā)過程中的不確定性，及時(shí)發(fā)現(xiàn)聯(lián)鎖軟件的設(shè)計(jì)缺陷，降低聯(lián)鎖軟件的開發(fā)成本。對(duì)于大中型站場(chǎng)，聯(lián)鎖邏輯關(guān)系非常復(fù)雜，如何建立正確的形式化驗(yàn)證模型，是聯(lián)鎖軟件中聯(lián)鎖邏輯關(guān)系形式化驗(yàn)證方法研究的重點(diǎn)。選岔網(wǎng)絡(luò)是保證聯(lián)鎖系統(tǒng)能夠正確選出滿足操作意圖的進(jìn)路的重要組成部分，為選岔網(wǎng)絡(luò)建立正確的形式化驗(yàn)證模型是聯(lián)鎖軟件形式化驗(yàn)證方法研究的重要內(nèi)容之一。

1 有色Petri網(wǎng)系統(tǒng)

1.1 CPN

Petri網(wǎng)是一種基于數(shù)學(xué)和圖形的描述分析工具，因其可使用圖形和嚴(yán)格的數(shù)學(xué)定義來描述系統(tǒng)，所以對(duì)系統(tǒng)結(jié)構(gòu)的描述較為容易，然而基本Petri網(wǎng)庫(kù)所中的Token屬于同一類型，個(gè)體之間沒有區(qū)別，對(duì)于大型復(fù)雜系統(tǒng)的建模容易造成狀態(tài)空間爆炸問題。有色Petri網(wǎng)（Colored Petri Net，CPN）是專門針對(duì)傳統(tǒng)Petri網(wǎng)的局限性，結(jié)合傳統(tǒng)Petri網(wǎng)的特征及高級(jí)編程語言的優(yōu)勢(shì)而發(fā)展起來的高級(jí)Petri網(wǎng)，主要由顏色集、聲明、庫(kù)所、變遷、弧、弧函數(shù)等組成，不僅具有直觀的圖形化表示，同時(shí)具有形式化的數(shù)學(xué)定義。在CPN中引入顏色集和分層的概念使得在使用CPN描述復(fù)雜系統(tǒng)結(jié)構(gòu)時(shí)能夠得到很大程度的簡(jiǎn)化，除此之外，CPN模型不僅可以直接描述異步并發(fā)系統(tǒng)的物理層次結(jié)構(gòu)及系統(tǒng)中各種資源的初始分布狀態(tài)，還可以展現(xiàn)出引發(fā)規(guī)則的作用下系統(tǒng)的動(dòng)態(tài)行為機(jī)理。因此在眾多的形式化建模方法和語言中，CPN建立的模型有利于動(dòng)態(tài)仿真，適合具有同步、并發(fā)、資源共享的復(fù)雜系統(tǒng)。

1.2 CPN TOOLS

CPN TOOLS是丹麥Aarhus大學(xué)CPN研究組開發(fā)的專用于CPN模型設(shè)計(jì)、仿真和分析的工具。CPN TOOLS能提供模型化、可視化的模型開發(fā)環(huán)境及友好交互界面，可在模型建立過程中自動(dòng)實(shí)現(xiàn)語法檢查和代碼生成，模型建立后，用戶可使用仿真工具，動(dòng)態(tài)執(zhí)行所建模型，同時(shí)生成仿真報(bào)告，CPN TOOLS提供的狀態(tài)空間分析功能，可對(duì)所建立的模型進(jìn)行部分或全部的狀態(tài)空間分析，生成的狀態(tài)空間報(bào)告包括可達(dá)性、有界性、活性、公平性、家態(tài)性等網(wǎng)的性質(zhì)。最新版本的cpn_tools 4.0.0在原有版本的基礎(chǔ)上又增加了約束弧及重置弧的功能，使得用CPN TOOLS建立系統(tǒng)模型更加方便。

2 選岔網(wǎng)絡(luò)

選岔網(wǎng)絡(luò)用于自動(dòng)選出進(jìn)路上道岔的位置，在繼電聯(lián)鎖中為了控制道岔的轉(zhuǎn)向，對(duì)應(yīng)每組道岔設(shè)置定位操縱繼電器（DCJ）和反位操縱繼電器（FCJ），分別控制道岔操縱到定位或反位，進(jìn)路選出的含義是指與所選進(jìn)路相關(guān)的所有的DCJ或FCJ都勵(lì)磁（不包括道岔的轉(zhuǎn)換），通過道岔的位置來確定進(jìn)路開通的方向。選岔網(wǎng)絡(luò)最重要的任務(wù)是必須能選出與操縱意圖一致的進(jìn)路。選岔網(wǎng)絡(luò)包括以下防護(hù)條件：

（1）確保道岔選出定位后不能再選反位，或者選出反位后不能再選定位。

（2）只有在與所排進(jìn)路所有相關(guān)道岔均處于解鎖狀態(tài)時(shí)才能選岔。

（3）在進(jìn)路不能選出時(shí)可以通過總?cè)∠姆绞饺∠x岔網(wǎng)絡(luò)的工作狀態(tài)。

（4）在車站值班員沒有辦理變通進(jìn)路時(shí)，只能選出基本進(jìn)路，而辦理了變通進(jìn)路后只能選出變通進(jìn)路，不能選出基本進(jìn)路。

以上防護(hù)條件只包含了對(duì)聯(lián)鎖邏輯關(guān)系做形式化驗(yàn)證建立CPN模型時(shí)所必須的防護(hù)條件，并不包含原繼電聯(lián)鎖電路中由于自身的電路原因而必需的防護(hù)條件。

3 選岔網(wǎng)絡(luò)CPN模型的建立

3.1 單動(dòng)道岔定、反位的CPN模型

根據(jù)6502電氣集中選岔電路可知雙動(dòng)道岔定位，單動(dòng)道岔定、反位在道岔操縱繼電器勵(lì)磁及自閉電路中所檢查的聯(lián)鎖條件是一致的，即必須有正負(fù)電源，道岔處于解鎖狀態(tài)，保證道岔處于正確的位置，保證在道岔不能鎖閉時(shí)能隨時(shí)取消，因此根據(jù)抽象出的聯(lián)鎖條件可為雙動(dòng)道岔定位，單動(dòng)道岔定、反位建立相似的CPN模型，本文以單動(dòng)道岔反位為例建立CPN模型如圖1所示。

由于單動(dòng)道岔反位控制的聯(lián)鎖條件較為簡(jiǎn)單，故建立的CPN模型也較為簡(jiǎn)單，模型中各顏色集均只包含一個(gè)元組，用CPN TOOLS提供的約束弧來滿足相關(guān)的聯(lián)鎖條件，庫(kù)所C、庫(kù)所Lock、庫(kù)所DC有Token時(shí)變遷src就不能發(fā)生，即道岔處于鎖閉狀態(tài)或道岔已操縱到定位或者進(jìn)路處于取消狀態(tài)時(shí)，均不能允許道岔操縱到反位。圖1中各庫(kù)所變遷的物理意義如表1所示。

圖1 單動(dòng)道岔反位控制的CPN模型圖

表1 單動(dòng)道岔反位控制各庫(kù)所變遷的物理意義一覽表

3.2 雙動(dòng)道岔反位控制的CPN模型

雙動(dòng)道岔反位可分為八字第一撇雙動(dòng)道岔反位及八字第二撇雙動(dòng)道岔反位，在繼電聯(lián)鎖電路中由于存在電路迂回，同極性電流串電現(xiàn)象，故把八字第一撇雙動(dòng)道岔反位、八字第二撇雙動(dòng)道岔反位分別設(shè)計(jì)在不同線的電路上。但是在CPN模型中不存在上述由于電路自身原因而導(dǎo)致的問題，故可以用同一種CPN模型來建立2種道岔反位控制的模型。雙動(dòng)道岔反位控制CPN模型如圖2所示。

圖2 雙動(dòng)道岔反位控制的CPN模型圖

圖2中各庫(kù)所變遷的物理意義如表2所示。

表2 雙動(dòng)道岔反位各庫(kù)所變遷的物理意義一覽表

3.3 變通進(jìn)路的CPN模型

進(jìn)路通常分為基本進(jìn)路和變通進(jìn)路，變通進(jìn)路又分為八字變通進(jìn)路及平行變通進(jìn)路，如何使得車站值班員能夠順利的選出與其操縱意圖一致的進(jìn)路，是在設(shè)計(jì)選岔網(wǎng)路時(shí)必須考慮的重點(diǎn)。

3.3.1 八字變通進(jìn)路的CPN模型

在繼電聯(lián)鎖控制中通過增設(shè)變通按鈕以及相應(yīng)的電路來選擇變通進(jìn)路，增設(shè)變通按鈕在選岔時(shí)的實(shí)質(zhì)主要是為選變通進(jìn)路時(shí)構(gòu)成兩段選路提供正負(fù)電源，借用6502的思想，在建立CPN模型時(shí)增設(shè)BKZ、BKF兩個(gè)庫(kù)所，為變通進(jìn)路的兩段選路提供正、負(fù)電源信號(hào)，以圖3所示的站場(chǎng)為例，建立經(jīng)5/7、17/19號(hào)道岔反位的變通進(jìn)路的CPN模型如圖4所示，由于不同站場(chǎng)中八字變通進(jìn)路所需的防護(hù)原理是相同的，故由此所建立的模型可用在所有的八字變通進(jìn)路中。

圖3 八字變通進(jìn)路示意圖

模型中由于每一段選路均涉及2組道岔，因此每一個(gè)提供電源信號(hào)的庫(kù)所均包含2個(gè)元組的托肯色，這2個(gè)元組雖然染上不同的顏色，但均表示為道岔操縱提供電源信號(hào)。與繼電聯(lián)鎖相似，在CPN模型中用相應(yīng)的約束弧作為同一組道岔定位操縱與反位操縱的互切條件，保證在變通進(jìn)路選不出時(shí)，不會(huì)自動(dòng)改選基本進(jìn)路。圖4所示的CPN模型中各庫(kù)所變遷的物理意義如表3所示。

圖4 八字變通進(jìn)路的CPN模型圖

表3 八字變通進(jìn)路CPN模型各庫(kù)所變遷的物理意義一覽表

3.3.2 平行變通進(jìn)路的CPN模型

在繼電聯(lián)鎖控制電路中通過斷線法來控制選出與值班員操縱意圖一致的平行變通進(jìn)路，在建立CPN模型時(shí)，不需要采用斷線法，但可借鑒繼電聯(lián)鎖電路中通過始端按鈕與變通按鈕、變通按鈕與終端按鈕相互配合選出變通進(jìn)路的方法來建立模型。因此建立模型的方法與八字變通進(jìn)路相似。

4 仿真及狀態(tài)空間分析

采用cpn_tools 4.0.0對(duì)圖1、圖2、圖4所建立的CPN模型進(jìn)行仿真，發(fā)現(xiàn)所有的模型均能通過語法檢查，在仿真的過程中既可對(duì)其進(jìn)行單步仿真操作，也可對(duì)其進(jìn)行連續(xù)仿真操作，通過仿真可知模型可以很好的模擬選岔工作，通過CPN TOOLS的Calculate State Space工具可進(jìn)行模型的狀態(tài)空間計(jì)算，同時(shí)自動(dòng)保存狀態(tài)空間報(bào)告。本文以圖3所建立的變通進(jìn)路的CPN模型為例對(duì)其狀態(tài)空間報(bào)告進(jìn)行分析。狀態(tài)空間報(bào)告節(jié)點(diǎn)統(tǒng)計(jì)、有界性、家態(tài)性、活性、公平性的截圖如圖5—圖7所示。

由圖5可知，對(duì)變通進(jìn)路選岔所建立的CPN模型所做的狀態(tài)空間分析是全部的狀態(tài)空間分析而不是部分的，由于有界性的狀態(tài)空間報(bào)告內(nèi)容較多，故只截取了其中的一部分，從圖6所示報(bào)告中可知各節(jié)點(diǎn)庫(kù)所的標(biāo)識(shí)數(shù)目有界，由此可知所建立的網(wǎng)模型是安全的，由圖7可知模型最終會(huì)終止在第441個(gè)節(jié)點(diǎn)，而該節(jié)點(diǎn)剛好是選岔結(jié)束的節(jié)點(diǎn)，說明選岔任務(wù)已完成，是符合功能邏輯的，通過多次仿真分析，發(fā)現(xiàn)系統(tǒng)都會(huì)終止在第441個(gè)節(jié)點(diǎn)上，這也驗(yàn)證了模型的家態(tài)性。報(bào)告中還可得到變遷的活性和托肯的活性，從報(bào)告中可知沒有死變遷，也沒有自動(dòng)觸發(fā)的變遷，這是因?yàn)檫x岔網(wǎng)絡(luò)的工作信息來源于外部，每次執(zhí)行完命令后均要等待下一次命令的到來，因此也不存在無限發(fā)生的序

列，這是與選岔網(wǎng)絡(luò)工作的邏輯功能相符的。

圖5 狀態(tài)空間節(jié)點(diǎn)統(tǒng)計(jì)截圖

圖6 狀態(tài)空間部分有界性截圖

圖7 狀態(tài)空間家態(tài)性、活性、公平性截圖

5 結(jié)論

本文在分析聯(lián)鎖系統(tǒng)選岔電路的基礎(chǔ)上抽象出選岔網(wǎng)絡(luò)的聯(lián)鎖條件，并根據(jù)這些聯(lián)鎖條件采用CPN對(duì)選岔網(wǎng)絡(luò)建立形式化分析模型，同時(shí)采用cpn_tools 4.0.0對(duì)模型進(jìn)行仿真及狀態(tài)空間分析，分析證明所建立的模型能夠很好的描述選岔網(wǎng)絡(luò)的功能邏輯。

[1] 袁崇義. Petri網(wǎng)應(yīng)用[M]. 北京：科學(xué)出版社，2013.

[2] 吳哲輝. Petri網(wǎng)導(dǎo)論[M]. 北京：機(jī)械工業(yè)出版社，2006.

[3] 袁崇義. Petri網(wǎng)原理及應(yīng)用[M]. 北京：電子工業(yè)出版社，2005.

[4] 林瑜筠，王孝義等. 6502電氣集中學(xué)習(xí)指導(dǎo)[M]. 北京：中國(guó)鐵道出版社，2006.

[5] 宮杰，陳邦興. 基于Petri網(wǎng)的聯(lián)鎖軟件測(cè)評(píng)仿真建模[J].計(jì)算機(jī)應(yīng)用與軟件，2009，26（2）：11-13.

[6] 陳邦興，吳芳美. 含過程和控制庫(kù)所的層次化Petri網(wǎng)模型及應(yīng)用[J]. 計(jì)算機(jī)應(yīng)用，2005，25（6），1410-1413.

[7] 陳邦興，吳芳美.鐵路信號(hào)聯(lián)鎖邏輯形式化建模研究[J].鐵道學(xué)報(bào)，2002，24（6）：50-54.

[8] 杜軍威，徐中偉，王素梅.聯(lián)鎖邏輯模型的安全性分析[J].計(jì)算機(jī)工程及應(yīng)用，2007，42（2）：1-4.

[9] M.S Durmus, M.T Soylemez, Railway Signlization and Interlocking Design via Automation Petri Nets, Proceedings of the 7th Asian Control Conference, HongKong, China. Augest 27-29,2009.

[10] Chen Xiang xian, HeYuLin, Huang hai. A component-based topology model for railway interlocking systems, Mathematics and Computers in Simulation 81 (2011) 1892-1900.

With detailed analysis of interlocking system switch selection circuit as a precondition, interlocking logic condition of switch selection network is abstracted, for which formalized verification model is established by adopting (colored Petri net CPN), simulation and status spatial analysis are made for the model established with CPN TOOLS, the results show that the working status of switch selection network is able to be well described by the established model.

Switch selection network; CPN; formalization; CPN TOOLS

U283

B

1007-936X(2015)02-0043-05

2014-06-09

陶 玲.重慶交通大學(xué)交通運(yùn)輸學(xué)院，碩士研究生，電話：18883861441；宋 軍.重慶交通大學(xué)信息科學(xué)與工程學(xué)院，教授。