【摘要】：礦井機(jī)車無(wú)人駕駛系統(tǒng)(UMLUS)的運(yùn)輸場(chǎng)景主要有：注冊(cè)啟動(dòng)、災(zāi)害防護(hù)、注銷、無(wú)線區(qū)段交接等,其中比較重要的是無(wú)線區(qū)段交接(WST)。WST實(shí)現(xiàn)礦井機(jī)車在相鄰WST管轄區(qū)段之間的安全交接功能,保證機(jī)車切換的無(wú)人值守,同時(shí)不會(huì)引起機(jī)車制動(dòng),實(shí)現(xiàn)平滑交接。采用形式化方法對(duì)無(wú)線區(qū)段交接過(guò)程進(jìn)行形式化建模與驗(yàn)證分析是保障系統(tǒng)安全性的一種手段。本文主要采用UML擴(kuò)展模型及層次有色Petri網(wǎng)對(duì)無(wú)線區(qū)段交接過(guò)程及其實(shí)時(shí)性能進(jìn)行驗(yàn)證分析,確保設(shè)計(jì)符合系統(tǒng)需求。本文通過(guò)將半形式化的UML建模方法與形式化的Petri網(wǎng)方法相結(jié)合,設(shè)計(jì)了基于UML擴(kuò)展模型及層次有色Petri網(wǎng)的UMLUS系統(tǒng)WST場(chǎng)景的建模與驗(yàn)證方法,通過(guò)UML模型進(jìn)行WST初步功能建模,再將層次有色Petri網(wǎng)作為該模型的驗(yàn)證方法,通過(guò)工具CPN Tools生成狀態(tài)空間報(bào)告,對(duì)模型的有界性、可達(dá)性、可達(dá)狀態(tài)空間進(jìn)行了分析驗(yàn)證。同時(shí)針對(duì)WST交接中的周期性通信交互消息的實(shí)時(shí)性特征設(shè)計(jì)了基于時(shí)間層次有色Petri網(wǎng)模型的UMLUS系統(tǒng)建模驗(yàn)證；WST過(guò)程中的通信采用｜WLAN方式,在軌道兩旁布設(shè)定向AP網(wǎng)絡(luò),在機(jī)車的運(yùn)行過(guò)程中會(huì)產(chǎn)生切換時(shí)延及突發(fā)中斷,通過(guò)仿真得出該過(guò)程的實(shí)時(shí)性能。
[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é)位級(jí)別】：碩士
【學(xué)位授予年份】：2015
【分類號(hào)】：TD67;TP301.1

【相似文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

，

本文編號(hào)：2243096