The Research Of Modeling And Verification Of Process Control For Mine Locomotive Running Based Event-B

As a typical safety critical system(SCS),the underground mine locomotive unmanned system(UMLUS)need to meet the requirements of high safety in designing processes.However,in the designing process of safety critical system software(SCSS),the traditional software engineering method is difficult to guarantee the requirements of completeness and consistency for the requirements document written by natural language,in the requirement analysis phase,and it also can't analyze and verify the correctness of the software sufficiently in the simulation and testing phase.These factors bring hidden troubles to the safety of the system.In order to solve the problems which is introduced by traditional software engineering methods,formal methods have been adopted.It can ensure the correctness of design and development for SCSS and the safety performance of the system.As a new formal method,the Event-B provides the step-by-step refinement strategy for modeling and the theorem proving method for model verification,which can help discover and repair the vulnerability of the system in advance,and it is of great significance for the development of SCSS.For the problems in the development of SCSS,we present a formal method based on Event-B,and researche the modeling and verification of locomotive running process controlling,which is the core function of the UMLUS.And the modeling and verification based on Event-B are studied for the locomotive mode selection process with discrete attributes and the locomotive autonomous driving process with discrete attributes and continuous attributes.The results show that the formal method based on Event-B can accurately describe the discrete attribute and continuous attribute requirements for locomotive running process control.It can also effectively find out the requirement vulnerability,such as requirements inconsistency,requirements missing and requirements fuzzy.In summary,the Event-B method can discover and make up these vulnerabilities in advance.And it also improves the safety of the SCSS.As a new idea for the development of the SCSS,it also provides a reference to the development of UMLUS.