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

Research on Event-B modeling and verification of signal system of locomotive transportation in mine

人工编制联锁表难以保证联锁表的准确性,而且单纯依靠人工检查联锁表中每个表项的正确性也是一项非常繁琐的工作。文章针对目前存在的问题,利用形式化Event-B方法对机车运输信号平面布置图、进路联锁表和机车车辆运输信号设计规范进行建模,模型生成的证明义务通过与否验证了进路联锁表建立过程是否符合平面布置图和设计规范的要求,利用该种思路解决了人工检查联锁表存在的效率低和不确定性等问题。

It is difficult to ensure the accuracy of the artificial interlocking table.Meanwhile,it is a very tedious work to manually check the correctness of each table item in the interlocking table.In view of the current problems,the modeling of the locomotive transportation signal plan,the route interlocking table and the design specifications for locomotive transportation signal is made by adopting Event-B method.And then whether the interlocking table complies with the plan and the design specifications is verified by using the proof obligations generated from those models,which solves the problems of inefficiency and uncertainty existed in manual inspection.