Formal Modeling And Verification Of Point Control Subsystem Based On B Method

This work takes the Point Control Subsystem as the research object,based on the system requirement specification,aiming at the functional safety issue,uses the B method to build a formal model of the system's functional logics,and completes the verification of the requirement specification,system function and decision-making process.This will enhance the credibility of the system.Based on the system requirements specification,the thesis analyzes the hazards of each module of the system and sorts out their demand meta-models,then analyzes the control process of the system,and then forms a data dictionary based on the existing demand meta-models,then uses the UPPAAL to quickly model the control process of the system.It can express the system control logic quickly,intuitively,dynamically and hierarchically,which is convenient for subsequent formal modelling.Before formal modelling,there needs to define the system modelling elements required for modelling,including various messages,sets,constants,static data relationships,and state variable data relationships.According to the Time-Automata model built by the UPPAAL tool,the formal B model modelling work of the system is carried out,and verify the safety properties of the B model,determine the correctness of the system design.Finally converting the verified B model into the C program Code.To visually observe the system functions and perform functional simulation,this thesis uses the Pro B to complete the graphical visualization of the model,and perform functional tests on the generated code to complete the final system validation.Based on the formalized B method,this thesis develops a system prototype of the Point Control Subsystem in a top-down way.The functional logic design of the system is verified in the Atelier B platform that supports the B method,and executable code is generated.Finally,the specific technical route of developing discrete control systems such as the point control subsystem using the B method is summarized.The technical route and development method used in this thesis can effectively improve the safety and reliability of the Point Control Subsystem,and have important reference significance to the development of other safety-critical systems.At the same time,it has demonstrative significance to the application and development of the formal method in the domestic rail transit field.