A Safety Analysis Method Based on Model Checking

With the development of equipment complexity and intelligence, the demand for safety analysis of equipment is constantly increasing. Traditional safety analysis methods mostly rely on human subjective judgment, so they lack objectivity and efficiency. Model checking is an automatic inspection method, which involves traversing the state space of a system through automated analysis and obtaining counterexamples ultimately. In this paper, we use model checking to address the aforementioned issues. We mainly make contributions in the following aspects. First of all, we study the determination and description methods of safety protocols. Then, we study the algorithm of model checking, focusing on the method of generating state space and state traversal. Next, we apply these methods to the wheel brake system and develop the programs. For ease of use, we develop a model checking tool, which can not only complete the generation of state space, but also verify the system model and output the safety analysis results automatically.