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

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

作　　者：荚文祥 陆阳[1] 许崇[1] 魏振春[1] JIA Wenxiang;LU Yang;XU Chong;WEI Zhenchun(School of Computer and Information,Hefei University of Technology,Hefei 230009,Chin)

机构地区：[1]合肥工业大学计算机与信息学院,安徽合肥230009

出　　处：《合肥工业大学学报（自然科学版）》2018年第6期787-794,共8页Journal of Hefei University of Technology：Natural Science

基　　金：国家重点研发计划资助项目(2016YFC0801804;2016YFC0801405);安徽省自然科学基金资助项目(1409085MKL79;1409085MKL80)

摘　　要：人工编制联锁表难以保证联锁表的准确性,而且单纯依靠人工检查联锁表中每个表项的正确性也是一项非常繁琐的工作。文章针对目前存在的问题,利用形式化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.

关 键 词：联锁表 Event-B方法 形式化方法 机车 证明义务 

分 类 号：TP399[自动化与计算机技术—计算机应用技术]