矿井机车无人驾驶系统无线区段交接过程形式化建模与验证研究
发布时间：2018-09-14 15:22
【摘要】：矿井机车无人驾驶系统(UMLUS)的运输场景主要有：注册启动、灾害防护、注销、无线区段交接等,其中比较重要的是无线区段交接(WST)。WST实现矿井机车在相邻WST管辖区段之间的安全交接功能,保证机车切换的无人值守,同时不会引起机车制动,实现平滑交接。采用形式化方法对无线区段交接过程进行形式化建模与验证分析是保障系统安全性的一种手段。本文主要采用UML扩展模型及层次有色Petri网对无线区段交接过程及其实时性能进行验证分析,确保设计符合系统需求。本文通过将半形式化的UML建模方法与形式化的Petri网方法相结合,设计了基于UML扩展模型及层次有色Petri网的UMLUS系统WST场景的建模与验证方法,通过UML模型进行WST初步功能建模,再将层次有色Petri网作为该模型的验证方法,通过工具CPN Tools生成状态空间报告,对模型的有界性、可达性、可达状态空间进行了分析验证。同时针对WST交接中的周期性通信交互消息的实时性特征设计了基于时间层次有色Petri网模型的UMLUS系统建模验证；WST过程中的通信采用｜WLAN方式,在轨道两旁布设定向AP网络,在机车的运行过程中会产生切换时延及突发中断,通过仿真得出该过程的实时性能。
[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.
【学位授予单位】：合肥工业大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TD67;TP301.1
本文编号：2243096
[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.
【学位授予单位】：合肥工业大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TD67;TP301.1
【相似文献】
相关会议论文 前1条
1 蔡远利;于振华;王瑞峰;;多Agent系统形式化建模方法学[A];'2006系统仿真技术及其应用学术交流会论文集[C];2006年
相关博士学位论文 前2条
1 陈永;基于高可信无线通信的列车流形式化建模与仿真[D];兰州交通大学;2014年
2 胡晓辉;智能分布监控系统软件形式化建模和设计研究[D];西北工业大学;2007年
相关硕士学位论文 前10条
1 任龙涛;基于STM嵌入式软件形式化建模及验证方法研究[D];大连理工大学;2015年
2 吕增威;矿井机车无人驾驶系统无线区段交接过程形式化建模与验证研究[D];合肥工业大学;2015年
3 夏倩倩;协同应用流程并行交互的形式化建模研究[D];内蒙古大学;2012年
4 肖知屹;列车安全距离控制形式化建模与验证[D];兰州交通大学;2014年
5 熊锡娇;列车自动防护系统的形式化建模与验证方法研究[D];华东师范大学;2012年
6 李丹;λ噬菌体生活周期的形式化建模与分析[D];上海交通大学;2007年
7 刘密霞;基于策略的信息安全模型及形式化建模的研究[D];兰州理工大学;2004年
8 周佳铭;基于PVS对SCADE开发轨交控制系统的形式化建模与验证[D];华东师范大学;2011年
9 濮阳;生物过程的形式化建模及仿真[D];上海交通大学;2007年
10 杨蒙;HMIPv6协议形式化建模及测试例生成方法研究[D];内蒙古大学;2010年
，本文编号：2243096
本文链接：https://www.wllwen.com/kejilunwen/kuangye/2243096.html
