基于混成自動機的礦井機車無人駕駛系統模型

衛 星, 王 軍

(合肥工業大學 計算機與信息學院,安徽 合肥 230009)

基于混成自動機的礦井機車無人駕駛系統模型

衛 星, 王 軍

(合肥工業大學 計算機與信息學院,安徽 合肥 230009)

礦井機車無人駕駛系統顯著表現出連續和離散同時存在的混成特征,混成自動機能夠精確刻畫其系統演化過程,文章研究該系統的建模及驗證問題。首先設定遵循安全高效駕駛原則的時間演化行駛過程模型;然后定義影響系統演化的各道岔信號燈狀態事件,并給出不同類型事件下的系統狀態轉換時刻遞推算法,從而得到系統混成自動機模型;最后以多種場景下的數值結果驗證了模型的正確性與完備性。

混成自動機;礦井機車;無人駕駛;混成系統;系統建模

混成系統是實時嵌入式系統的一種重要子類,其行為中廣泛存在離散控制邏輯跳轉與連續實時行為交織混雜的情況[1]。礦井機車無人駕駛系統包括遠程遙控與自動駕駛2種模式：遠程遙控駕駛是利用井下移動無線網絡WLAN,將礦井機車行進方向的視頻與運行狀態數據實時傳輸到地面運輸調度中心與遙控駕駛臺,工作人員在地面運輸調度中心利用遙控操作臺遙控機車與井下相關設備進行生產作業;自動駕駛是機車依靠車載計算機與路況分析器自主行駛,無需駕駛人員干預。該系統避免了在發生礦井坍塌或機車相撞事故時出現人員的傷亡,使機車能夠可靠地在井下運輸調度并保障工作人員的安全[2]。礦井機車無人駕駛系統既要處理連續的位置和速度變量,又要處理機車運行狀態、遠程遙控指令和信號燈狀態等離散變量,具有混成系統的典型特征。

對混成系統的分析(如可靠性、可達性等)是建立在對其行為合理建模的基礎之上。而混成自動機是一種廣泛應用且能夠精確刻畫混成系統連續和離散動態行為的建模語言，其相關研究目前集中于交通、工業過程控制、國防等領域控制系統的建模與分析。文獻[3]針對CTCS-3級列控系統的混合性,提出基于混成自動機的建模方法,并使用Simulink和Stateflow 對建立的模型進行仿真驗證;文獻[4]利用線性混成自動機形式化方法對列車控制系統(communication-based train control system, CBTC)中的ZC子系統進行建模分析與性質驗證;文獻[5]針對汽車信息物理融合系統(cyber-physical system, CPS)軟件的異構性、分布式等特點,提出了基于混成自動機的車聯網服務建模方法;文獻[6]建立了基于TCP-Ren擁塞控制版本和RED路由算法的混成自動機模型;文獻[7]在礦井機車運輸監控系統調度聯鎖基本規則的基礎上,采用有色Petri網對其聯鎖過程進行建模與分析;文獻[8]對金屬礦山井下單軌運輸系統進行了建模并使用改進后的遺傳算法對其進行優化,使得系統運輸效率有了較大程度的提高。

本文使用混成自動機對礦井機車無人駕駛系統進行建模與分析。通過簡化實際工程系統的結構,并在引入時間演化和事件驅動2種機制共同作用的基礎上,得到系統的混成自動機模型及狀態轉移圖,最后通過數值計算給予驗證。

1 礦井機車無人駕駛系統結構

礦井機車無人駕駛系統,主要由礦井機車、移動寬帶流媒體網絡、機車運行服務器、遙控操作臺、遙控操作盒、遙控料斗和定標器等設備組成。駕駛人員在地面運輸調度中心借助遙控操作臺操控機車,實時執行調度系統調度意圖。為了保證運輸安全和提高運輸效率,機車一次運輸任務從起點到終點的全部路徑被劃分為若干相對固定的進路,作為調度分配和機車占用的單位,通常每條進路會分配1個固定的進路號。1條進路在正常運行時只能被1輛機車占用,以避免機車相撞。

無人駕駛機車的整體控制流程分為信息獲取、信息處理、設備控制3個部分,如圖1所示。在機車運行過程中,機車控制器依據定標接收器收到的定標點信息和車速傳感器檢測到的脈沖信號計算運行速度及所在位置(離定標點的距離),根據通過網絡接收的行車指令及路況分析器發來的路況信息,結合運行模式及預存的運行參數進行綜合分析、判斷，生成操作命令,通過Modbus接口發送給變頻控制柜,控制機車的運行,同時機車控制器還將機車運行狀況(包括進路位置、行車速度、運行方向等)通過網絡上報給地面調度系統。

信息獲取階段,機車控制器的信息來源可分為地面設備、車載設備2個部分;信息處理階段,機車控制器根據信息獲取階段獲取的信息進行分析判斷,向變頻器發送控制指令,進行調速、鳴笛、駐車、供電等控制;設備控制階段,變頻器根據機車控制器發來的控制指令,完成對牽引電機、喇叭、駐車推桿、受電弓推桿的控制。

圖1 無人駕駛機車控制流程

2 模型設定與分析

2.1 模型設定

設機車在0時刻從原點(即進路r1起始處)靜止啟動,在t時刻其加速度、速度、位移分別為a(t)、v(t)、x(t)。其中,a(t)由發動機牽引力、車輪制動力、軌面摩擦力和列車質量共同作用產生,a(t)∈[amin,amax],amin<0表示最大減速度,amax>0表示最大加速度。機車在進路ri(i=1,2,…,n)內行駛的限速值為vi。當機車到達終點時加速度、速度為0。

圖2 系統模型設定程

機車的遠程駕駛過程描述如下。

(1) 信號燈RGi為綠燈(RGi=1)且在讀秒歸零前機車已到達該信號燈處,或信號燈RGi為紅燈(RGi=0)且在讀秒歸零時機車還未到達,機車以vi勻速駛過該信號燈。

(2) 信號燈RGi為綠燈(RGi=1)且在讀秒歸零前機車不能到達該信號燈處,或信號燈RGi為紅燈(RGi=0)且在讀秒歸零前機車已達,機車減速并停駛在該信號燈前。

(3) 未目測到信號燈,即進入最末進路rn,機車減速并停駛在該進路末端。

2.2 模型分析與算法

圖3 進路ri運行時段示意

(1)

(2)

(3)

(4)

(5)

(6)

(7)

(8)

(9)

(2) 執行各輪次。

do{

if(i∈E1∪E2)//信號燈RGi屬于的事件集

else if(i∈E3)

else if(i∈E4)

else if(i∈E5)//此時機車處于此次運輸任務路段的最后一個進路內

i++//機車進入下一進路

}while(i≤n)

(10)

3 系統混成自動機建模

礦井機車無人駕駛系統混成自動機建模[9-10]如下:

(1) 機車在行駛過程中共經歷了n+3種狀態(加速狀態、減速狀態、靜止狀態、勻速v1、勻速v2、…、勻速vn)之間的跳變,即Ω={Acc,Dec,Sti,Uni-v1,Uni-v2,…,Uni-vn},它們構成了狀態圖中的節點。

(2) Σ為離散事件的有限集合,影響機車行駛過程的5種不同類型n-1個事件,構成了模型離散事件的有限集合,即Σ={E1,E2,E3,E4,E5}。

(5)L0?L為初始位置的集合,機車在執行1次運輸任務的初始狀態為靜止狀態,即L0={Sti}。

系統混成自動機狀態轉移圖如圖4所示。

圖4 系統混成自動機狀態轉移圖

4 數值分析

4.1 參數設定

本文采用文獻[11-12]的基于離散事件系統的仿真方法,所設定的機車運行場景來源于安徽開發礦業有限公司李樓鐵礦-425 m運輸巷道,如圖5所示,處于進路r1的機車將要前往裝料區進行一次裝料運輸任務,機車通過進路r1→r2→r3→r4→r5到達裝料區。電機車采用典型的變頻方式調速,其中線性加速度適用于需要平穩地傳動或緩慢加/減速的大部分場合。

圖5 李樓-425 m礦井部分巷道水平面運輸示意圖

根據以上內容設定參數如下。

(1) 進路長度。l1=850 m,l2=1 000 m,l3=1 250 m,l4=1 200 m,l5=900 m。

(2) 每一進路區間內機車行駛的限速值。v1=4.0 m/s,v2=3.0 m/s,v3=5.0 m/s,v4=3.5 m/s,v5=2.0 m/s。

(3) “駕駛員”目測距離S=40 m。

(4) 機車行駛過程中加速時的最大加速度amax=0.1 m/s2,剎車時的最大減速度amin=-0.2 m/s2。

(5) 信號燈紅綠轉換周期。T1=350 s,T2=250 s,T3=350 s,T4=450 s。

4.2 實驗結果和分析

圖6 場景A機車速度-時間關系

圖7 場景B機車速度-時間關系

圖8 2種場景下機車位移-時間關系

5 結 論

本文以多進路運輸路徑的無人駕駛礦井機車為研究對象,首先設定遵循安全高效駕駛原則的時間演化行駛過程模型;然后定義影響系統演化的各信號燈狀態事件,并給出不同類型事件下的系統狀態轉換時刻遞推算法,從而得到系統混成自動機模型;最后以多種場景下的數值結果驗證了模型的正確性與完備性。

本文研究機車在無障礙物事件影響情況下的行駛過程,當進一步考慮加入障礙物,發生另一離散事件時,可以將其等同于進路之間的信號燈事件來分析,若障礙物出現在機車的前方,其到機車的距離小于機車以最大減速度減速到靜止時所經過的位移,機車必然撞上障礙物,跳轉到故障狀態。

[1] 卜磊,謝定寶.混成系統形式化驗證[J].軟件學報,2014,25(2):219-231.

[2] 鄧軍,李貝,李海濤,等.中國礦山應急救援體系建設現狀及發展芻議[J].煤礦開采,2013,18(6):5-9.

[3] 易承龍,李開成.基于混雜系統理論的CTCS-3 級列控系統建模與仿真[J].計算機應用與軟件,2014,31(10):67-69.

[4] 侯曉鵬.基于混成自動機的ZC子系統安全的驗證方法研究[D].北京:北京交通大學,2015.

[5] 封飛,陳名才,張廣泉,等.基于混成自動機的車聯網服務建模方法[J].南通大學學報(自然科學版),2013,12(6): 6-10.

[6] 吳志偉,袁德成,韓坤.基于混雜自動機的TCP網絡擁塞控制模型[J].儀器儀表學報,2006,27(增刊3):2001-2003.

[7] 陸陽,郭智奇,韓江洪,等.礦井機車運輸監控系統調度聯鎖過程的Petri網建模[J].煤炭學報,2007,32(11):1216-1223.

[8] 謝新穎,魏鏡弢,張嘯海.金屬礦山井下單軌運輸系統建模及優化[J].金屬礦山,2012(2):124-126.

[9] MAHEMUTI P,YANG L,LUO L L.Modeling,analysis and synthesis of hybrid system: a review[J].Applied Mechanics and Materials,2014,615:36-43.

[10] 劉攀,繆淮扣,曾紅衛,等.基于FSM的測試理論、方法及評價[J].計算機學報,2011,34(6):965-984.

[11] MAGOTT J,SKROBANEK P.Timing analysis of safety properties using fault trees with time dependencies and timed state-charts[J].Reliability Engineering & System Safety,2012,97(1):14-26.

[12] BAK S,BOGOMOLOV S,JOHNSON T T.HYST: a source transformation and translation tool for hybrid automaton models[C]//18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015).[S.l.]:ACM,2015:128-133.

(責任編輯 張淑艷)

Model of unmanned driving system of mine locomotive based on hybrid automaton

WEI Xing, WANG Jun

(School of Computer and Information, Hefei University of Technology, Hefei 230009, China)

The composite character of simultaneous existence of sequence and discreteness is shown in the unmanned driving system of mine locomotive. The system evolution can be depicted accurately by hybrid automaton. The modeling and verification of the system is researched. Firstly, the driving process model with time evolution is set which follows the principle of safe and efficient driving. Then the state events of each turnout signals that affect the system evolution are defined. The recursive algorithm of conversion time of the system under the different types of events is given. And the hybrid automaton model of the system can be obtained. Finally, the accuracy and completeness of the model are verified by the numerical results in various situations.

hybrid automaton; mine locomotive; unmanned driving; hybrid system; system modeling

2016-02-02；

2016-04-18

國家國際科技合作專項資助項目(2014DFB10060)

衛 星(1980-),男,安徽肥西人,博士,合肥工業大學副教授,碩士生導師.

10.3969/j.issn.1003-5060.2017.08.007

TP399

A

1003-5060(2017)08-1042-06