Modeling and verification of running process control for underground mine locomotive. (October 2020) - Zhu, Siwei; Zhang, Jianjun; Zhao, Sulei; Wei, Zhenchun; Lu, Yang; Cheng, Lei
Abstract: The traditional underground mine locomotive unmanned system is difficult to define requirements accurately and guarantee the functional safety and integrity. To solve this problem, a solution based on Event-B formal method is put forward. In this paper, we select the locomotive running process control for formal modeling and verification, which is the core of the underground mine locomotive unmanned system. Based on the Event-B formal method and Rodin platform, five refinements are proposed to model and verify the locomotive running process control with both discrete and continuous attributes. The correctness, consistency and deadlock-freeness of the system design in the actual situation are verified with extensive simulations. The verification and simulation results show that the solution meets the design requirements of the running process control of the underground mine locomotive. Graphical abstract: Highlights: A solution of the Event-B method is explored to improve the accuracy of safety critical system. The formal modeling and verification of mine locomotive running process control based on Event-B is put forward with five refinements. Both discrete attributes and continuous attributes of locomotive running process control are considered. The obligation and deadlock-freeness of the system are verified with the Rodin platform and ProB plug-in respectively.