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

陶 玲，宋 軍

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

陶 玲，宋 軍

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

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

0 引言

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

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

1.1 CPN

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

1.2 CPN TOOLS

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

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

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

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

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

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

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

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

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

3.1 單動道岔定、反位的CPN模型

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

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

圖1 單動道岔反位控制的CPN模型圖

表1 單動道岔反位控制各庫所變遷的物理意義一覽表

3.2 雙動道岔反位控制的CPN模型

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

圖2 雙動道岔反位控制的CPN模型圖

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

表2 雙動道岔反位各庫所變遷的物理意義一覽表

3.3 變通進路的CPN模型

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

3.3.1 八字變通進路的CPN模型

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

圖3 八字變通進路示意圖

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

圖4 八字變通進路的CPN模型圖

表3 八字變通進路CPN模型各庫所變遷的物理意義一覽表

3.3.2 平行變通進路的CPN模型

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

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

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

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

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

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

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

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

5 結(jié)論

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

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

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

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

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

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

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

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

[8] 杜軍威，徐中偉，王素梅.聯(lián)鎖邏輯模型的安全性分析[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

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