矿井机车运输信号系统的Event-B建模与验证研究

摘要

运输信号系统设计时,应根据机车车辆的运行图表、运行方式、行车组织情况、巷道及运输线路平面图等绘制运输信号平面布置图,编制联锁表.人工编制联锁表难以保证联锁表的准确性,而且单纯依靠人工检查联锁表中每个表项的正确性也是一项非常繁琐的工作.针对目前存在的问题,利用形式化Event-B方法对矿井机车运输信号系统进行建模,通过模型生成的证明义务来自动验证联锁表,解决了人工检查联锁表存在的效率低和不确定性等问题.