矿井机车自主驾驶过程的建模及验证  

Modeling and verification of autonomous driving process of mine locomotive

作　　者：赵雷 卫星[1] 张建军 ZHAO Lei;WEI Xing;ZHANG Jianjun(School of Computer and Information,Hefei University of Technology,Hefei 230009,China)

机构地区：[1]合肥工业大学计算机与信息学院,安徽合肥230009

出　　处：《合肥工业大学学报（自然科学版）》2018年第10期1362-1367,共6页Journal of Hefei University of Technology：Natural Science

基　　金：国家重点研发计划资助项目(2016YFC0801405;2016YFC0801804)

摘　　要：文章首先使用自然语言描述了矿井机车自主驾驶系统的结构和控制过程;然后基于时间自动机理论对自主驾驶中涉及的机车控制器、机车运行服务器以及其他车载设备、被控对象建模,从而得到自主驾驶的时间自动机网络模型;最后应用时间自动机模型验证工具UPPAAL对自主驾驶模型进行了仿真分析和验证。验证结果表明建立的模型满足系统的功能性需求和实时性需求,证明了系统设计的正确性。In this paper,the natural language description of the structure and control process of mine locomotive autonomous driving system is made.Then the objects such as locomotive controller,train operation server,controlled objects and other vehicle on-board equipment involved in the autonomous driving process are modeled based on the theory of timed automata(TA),thus a TA network model of the autonomous driving process of mine locomotive is obtained.Finally,the TA verification tool UPPAAL is used for the simulation and validation.The validation results show that the established model meets the requirements of qualitative and timed bounded liveness properties,thus proving the correctness of system design.

关 键 词：时间自动机 UPPAAL工具 模型检测 矿井机车 自主驾驶 系统建模 

分 类 号：TP391.9[自动化与计算机技术—计算机应用技术]