Research On Analysis And Verification Of Design Of Underground Locomotive Transportation Signal Based On Event-B Method

At present,There are many problems that technology is not mature enough in the coal mining industry in China,such as the low degree of mechanization,low degree of automation and low degree of informatization,which is one of the main factors that lead to the frequent occurrence of coal mine accidents.As one of the important links in the process of underground coal mining,the mine locomotive transportation plays an important role in improving the production efficiency.The design of the mine locomotive transport signal system is directly related to whether the locomotive transport signal can organize the locomotive transportation in time and accurately,establish the transportation order,ensure the traffic safety,and complete the transportation task,the design of the interlocking table is the key part of the design process of the transport signal system,and its standardization affects the design of the whole system to a great extent.The code for design of underground locomotive vehicle transport signal of coal mine is the basic document of constraint plane layout diagram of transport signal and interlocking table.In order to accurately design the interlocking table that conform to design code,firstly,the dissertation analyzes the current shortcomings that mainly rely on manual detection of interlocking table,put forward using Event-B formal language for modeling design code,plane layout diagram and interlocking table.For the abstract part of the model of the plane layout diagram and interlocking table is input into the Rodin platform in advance,the concrete implementation of the abstract content of model is based on the specific plane layout diagram and interlocking table,the process of the specific implementation is use the Rodin platform extendibility,installing WindowBuilder Java Core plugin in the platform,so we can use variety of interface functions from Java language to operate Excel table content,therefor model of a specific plane layout diagram and interlocking table can be built automatically and input into Rodin platform.Secondly,the dissertation introduce the main content of the code for design of underground locomotive vehicle transport signal of coal mine,including design of district,route and interlocking,signal,turnout and switch device,position sensor and radio receiving/transmitting device.Selecting the rules about signal interlock to model,and finally complete the whole model of mine locomotive transport signal system.Finally,the dissertation studies the core of Event-B,and then analyzes the principle of using model to verify and detect the interlocking table.The Event-B model of the mine locomotive transport signal system can generate the THM proof obligation rule in the proof generator,proved by ProB plugin in the Rodin platform.In the process of proof,the platform outputs the corresponding prompt information,through the information to verify and detect the interlocking table.So it overcome the shortcomings of manual verification of interlocking table,and improve the design efficiency of mime locomotive transport signal system.The results show that the Event-B method can be better used in locomotive transportation signal system modeling and verification and detection process of interlocking table.