【摘要】：礦井機(jī)車無人駕駛系統(tǒng)(UMLUS)的運(yùn)輸場景主要有：注冊啟動、災(zāi)害防護(hù)、注銷、無線區(qū)段交接等,其中比較重要的是無線區(qū)段交接(WST)。WST實現(xiàn)礦井機(jī)車在相鄰WST管轄區(qū)段之間的安全交接功能,保證機(jī)車切換的無人值守,同時不會引起機(jī)車制動,實現(xiàn)平滑交接。采用形式化方法對無線區(qū)段交接過程進(jìn)行形式化建模與驗證分析是保障系統(tǒng)安全性的一種手段。本文主要采用UML擴(kuò)展模型及層次有色Petri網(wǎng)對無線區(qū)段交接過程及其實時性能進(jìn)行驗證分析,確保設(shè)計符合系統(tǒng)需求。本文通過將半形式化的UML建模方法與形式化的Petri網(wǎng)方法相結(jié)合,設(shè)計了基于UML擴(kuò)展模型及層次有色Petri網(wǎng)的UMLUS系統(tǒng)WST場景的建模與驗證方法,通過UML模型進(jìn)行WST初步功能建模,再將層次有色Petri網(wǎng)作為該模型的驗證方法,通過工具CPN Tools生成狀態(tài)空間報告,對模型的有界性、可達(dá)性、可達(dá)狀態(tài)空間進(jìn)行了分析驗證。同時針對WST交接中的周期性通信交互消息的實時性特征設(shè)計了基于時間層次有色Petri網(wǎng)模型的UMLUS系統(tǒng)建模驗證；WST過程中的通信采用｜WLAN方式,在軌道兩旁布設(shè)定向AP網(wǎng)絡(luò),在機(jī)車的運(yùn)行過程中會產(chǎn)生切換時延及突發(fā)中斷,通過仿真得出該過程的實時性能。
[Abstract]:The transportation scenarios of mine locomotive unmanned system (UMLUS) mainly include: registration startup, disaster prevention, cancellation, wireless section handover, etc. It is more important that the wireless section handover (WST). WST realizes the safe transfer function of mine locomotive in the adjacent WST section, ensures the locomotive switch unattended, at the same time does not cause locomotive brake, realizes smooth handover. Formal modeling and verification analysis of wireless segment transition process is a method to ensure the security of the system. In this paper, the extended UML model and the hierarchical colored Petri network are used to verify and analyze the wireless segment transition process and its real-time performance to ensure that the design meets the requirements of the system. By combining the semi-formal UML modeling method with the formal Petri net method, this paper designs the WST scene modeling and verification method of UMLUS system based on UML extension model and hierarchical colored Petri net, and uses UML model to model the initial function of WST. Then the hierarchical colored Petri net is used as the verification method of the model, and the boundedness and reachable state space of the model are analyzed and verified by using the tool CPN Tools to generate the state space report. At the same time, aiming at the real-time characteristics of the periodic communication interactive messages in the WST handover, the modeling of UMLUS system based on the time-level colored Petri net model is designed. The communication in the UMLUS process is based on the WLAN mode, and the oriented AP network is arranged on both sides of the track. Switching delay and sudden interruption will occur during locomotive operation. The real-time performance of the process is obtained by simulation.
【學(xué)位授予單位】：合肥工業(yè)大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：TD67;TP301.1

【相似文獻(xiàn)】

相關(guān)會議論文 前1條

1 蔡遠(yuǎn)利;于振華;王瑞峰;;多Agent系統(tǒng)形式化建模方法學(xué)[A];'2006系統(tǒng)仿真技術(shù)及其應(yīng)用學(xué)術(shù)交流會論文集[C];2006年

相關(guān)博士學(xué)位論文 前2條

1 陳永;基于高可信無線通信的列車流形式化建模與仿真[D];蘭州交通大學(xué);2014年

2 胡曉輝;智能分布監(jiān)控系統(tǒng)軟件形式化建模和設(shè)計研究[D];西北工業(yè)大學(xué);2007年

相關(guān)碩士學(xué)位論文 前10條

1 任龍濤;基于STM嵌入式軟件形式化建模及驗證方法研究[D];大連理工大學(xué);2015年

2 呂增威;礦井機(jī)車無人駕駛系統(tǒng)無線區(qū)段交接過程形式化建模與驗證研究[D];合肥工業(yè)大學(xué);2015年

3 夏倩倩;協(xié)同應(yīng)用流程并行交互的形式化建模研究[D];內(nèi)蒙古大學(xué);2012年

4 肖知屹;列車安全距離控制形式化建模與驗證[D];蘭州交通大學(xué);2014年

5 熊錫嬌;列車自動防護(hù)系統(tǒng)的形式化建模與驗證方法研究[D];華東師范大學(xué);2012年

6 李丹;λ噬菌體生活周期的形式化建模與分析[D];上海交通大學(xué);2007年

7 劉密霞;基于策略的信息安全模型及形式化建模的研究[D];蘭州理工大學(xué);2004年

8 周佳銘;基于PVS對SCADE開發(fā)軌交控制系統(tǒng)的形式化建模與驗證[D];華東師范大學(xué);2011年

9 濮陽;生物過程的形式化建模及仿真[D];上海交通大學(xué);2007年

10 楊蒙;HMIPv6協(xié)議形式化建模及測試?yán)煞椒ㄑ芯縖D];內(nèi)蒙古大學(xué);2010年

，

本文編號：2243096