论文部分内容阅读
我国目前煤矿开采业存在机械化、自动化、信息化程度低等技术不够成熟的问题，是导致煤矿事故频发的主要因素之一。矿井机车运输作为煤矿井下开采过程中的重要一环，它对提高生产效率起到关键作用。矿井机车运输信号系统设计的优良与否直接关系到机车运输信号能否及时准确地组织机车运输、建立运输秩序、保证行车安全、完成运输任务，而联锁表的设计是运输信号系统设计过程中关键的部分，它的规范性与否很大程度上影响到整个系统设计的优劣。 煤矿井下机车车辆运输信号设计规范是约束运输信号平面布置图和联锁表的基础性文件。为了精确的设计出符合设计规范的联锁表，本文首先分析了目前主要依靠人工检测联锁表的弊端，提出了利用Event-B形式化语言对设计规范、平面布置图和联锁表进行建模。其中，对于平面布置图和联锁表模型中的抽象部分事先输入Rodin平台中，而具体实现模型抽象内容是根据具体的平面布置图和联锁表完成的，实现过程中利用了Rodin平台的可扩展性，在平台中安装WindowBuilderJava Core插件，从而可以利用Java语言的多种接口函数来操作Excel表格内容，实现具体的平面布置图和联锁表自动生成模型内容并输入到Rodin平台中。其次，介绍了《煤矿井下机车车辆运输信号设计规范》的主体内容，包括区段、进路与联锁设计，信号机，道岔与转辙装置，车位传感器与无线收发信装置，筛选出关于信号联锁的规则进行建模，最终完成矿井机车运输信号系统的全部模型。最后，本文研究了Event-B的核心内容，进而分析了利用模型验证和检错联锁表的原理。 矿井机车运输信号系统的Event-B模型在证明义务生成器中可以生成THM证明义务规则，通过Rodin平台中的ProB插件可证明THM，证明过程中平台输出相应的提示信息，通过信息实现验证和检测联锁表的目的，从而克服了人工验证联锁表时存在不确定性的缺点，同时也提高了矿井机车运输信号系统的设计效率。结果表明，Event-B方法能较好的运用于机车运输信号系统的建模以及联锁表验证与检错过程。