矿井机车无人驾驶系统在设计时具有较高的安全要求,属于典型的安全关键系统。然而,在安全关键系统软件的设计过程中,传统上基于软件工程的方法,一方面,在需求分析阶段,由于自然语言编写的需求文档难以保证需求的完备性和一致性,另一方面,仿真和测试的也无法保证软件分析和验证的完全正确,这些因素给系统的安全带来了隐患。目前,针对传统软件工程方法在开发安全关键系统中遇到的问题,科研人员采用形式化方法来保证安全关键系统软件设计的正确性,进而提高系统的安全性。Event-B作为一种全新的形式化方法,具有逐步精化的建模策略和基于定理证明的模型验证方式。通过采用Event-B方法对安全关键系统软件进行建模与验证可以更早发现并修复系统的漏洞,对于安全关键系统软件的开发具有重要的借鉴意义。本文针对安全关键系统软件——矿井机车无人驾驶系统研发中遇到的问题,提出了基于Event-B形式化方法的解决方案,并选取矿机机车无人驾驶系统的核心功能——机车运行过程控制进行了形式化建模与验证的探索研究。分别对只具有离散属性的机车模式选择过程,和既具有离散属性又具有连续属性的机车自主行车过程控进行了基于Event-B方法的建模与验证。本文的研究结果表明,基于Event-B形式化方法可以准确的描述机车运行过程控制中的离散属性和连续属性需求。同时,通过定理证明的方式可以有效发现需求文档中存在的需求不一致性、需求缺失和需求模糊等问题,进而提早发现并修正这些漏洞,有效的提高了系统设计的正确性,为矿井机车无人驾驶系统的研发提供了一种借鉴,同时也为安全关键系统软件的研发提供了一种新的思路。