矿井机车无人驾驶系统可以有效减少井下作业人员,降低矿井安全事故伤亡,对安全生产具有重要意义。作为一种安全关键系统,其对安全性有很高的要求,在系统设计阶段采用形式化方法进行验证十分必要。本文针对矿井机车无人驾驶系统的特点,提出一种对由多个子系统构成,要求故障-安全性的矿井机车无人驾驶系统进行建模与验证的方法,并利用该方法对矿井机车自主驾驶和遥控驾驶过程进行了建模和验证。论文完成的主要工作如下:(1)基于运行场景对矿井机车无人驾驶过程进行分析,针对矿井机车无人驾驶过程中的数据特点,提出了基于数据表的数据交互方案和无人驾驶机车控制过程的总体流程。(2)针对矿井机车无人驾驶系统特点,本文提出了对其设计方案正确性进行建模及验证的方法。该方法分为五个步骤,第一,确定验证需求;第二,模型基础数据定义,这些数据用于驱动矿井机车无人驾驶模型运行;第三,模型分解,对于建模过程中复杂对象的建模,采用模型分解的方法降低单个模型复杂度;第四,模型构建,在方法中介绍了模型中语法元素与系统设计内容之间的对应关系;第五,模型检测。(3)基于本文提出的方法,对矿井机车自主驾驶过程和遥控驾驶过程进行了建模验证。自主驾驶过程模型主要由数据采集设备模型、执行机构模型、机车控制器和机车运行服务器模型组成,由于机车控制器功能的复杂性,将其划分为数据获取、控制决策、控制执行三个过程分别建模,建模完成后,在Uppaal中对模型进行验证,证明了系统设计的正确性。对遥控驾驶过程的建模分为绑定和控制两个过程,本文主要分析控制过程,模型主要涉及驾驶员、机车控制器、遥控操作台、机车运行服务器等,在建模过程中考虑了设备故障、网络丢包及时延等因素,最后在遥控驾驶过程模型中验证遥控驾驶过程设计的正确性。