Modeling and verification of running process control for underground mine locomotive. (October 2020)

• Record Type: Journal Article
• Authors: Zhu, Siwei; Zhang, Jianjun; Zhao, Sulei; Wei, Zhenchun; Lu, Yang; Cheng, Lei
• Is Part Of: Computers & electrical engineering. Volume 87(2020)
• Publication Date: 2020-10
• Subjects: Unmanned system -- Underground mine locomotive -- Event-B -- Formal modeling -- Formal verification; Computer engineering -- Periodicals; Electrical engineering -- Periodicals; Electrical engineering -- Data processing -- Periodicals; Ordinateurs -- Conception et construction -- Périodiques; Électrotechnique -- Périodiques; Électrotechnique -- Informatique -- Périodiques; Computer engineering; Electrical engineering; Electrical engineering -- Data processing; Periodicals; Electronic journals; 621.302854
• DOI: 10.1016/j.compeleceng.2020.106790
• Languages: English
• ISSNs: 0045-7906

Abstract

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.