Research On Modeling And Verification Of Safety-critical Systems Based On Formal Methods

Safety-critical systems refer to systems that have extremely high requirements for safety and reliability.The normal operation of safety-critical systems relies heavily on correct functional scenarios and control logic,making it crucial to ensure the correctness of these scenarios and logic using effective methods.Formal methods are a mathematical-based system development and verification technique that possesses rigorous logical reasoning capabilities.They can identify errors and defects in the functional scenarios and control logic of a system,thereby improving system design and enhancing system safety and reliability.With the development of society and advancements in technology,safety-critical systems are continuously expanding in scale,leading to an increased risk of defects and vulnerabilities.Therefore,the introduction of formal methods,which describe system functionality and properties using rigorous mathematical logic,is of significant practical importance for the security verification of safety-critical systems.In this paper,the level crossing control system,a typical safety-critical system,is selected as the research object.Certain improvements are made to address the defects in traditional level crossing control systems.A formal model compatible with the improved level crossing control system is designed and implemented,followed by formal verification of the model.The research achievements of this paper can be summarized as follows:1.A comprehensive analysis of the functionality and defects of general level crossing control systems is conducted,and a system improvement plan is proposed to address the existing defects.The improved system solves three major problems:continuous train collision,pedestrian and vehicle blockage,and insufficient reserve braking distance.Based on the components and functionality of the improved system,control specifications that ensure reliability in the system control flow are extracted,enabling an abstract description of the level crossing control system.2.A formal model for the improved level crossing control system is designed.The model is constructed using the EVENT-B language,following a stepwise refinement modeling approach.It consists of an initial model and four refinement levels,resulting in a model that can be applied to most level crossing control systems.3.Formal verification of the level crossing control system is conducted using both automated and interactive proof methods.The effectiveness of various functions in the established model is verified through invariant proof and Pro B simulation.The verification results demonstrate that all functions of the model operate correctly,ensuring safety and reliability,thus laying the foundation for code-level development of the level crossing control system.