Development Of Point State Monitoring Unit Based On Formal Method And Verification Of Logic Decision Process

This thesis takes the point state monitoring unit as the research object,aiming at solving the safety decision-making of railway system under the background of intelligence.In this thesis,the logic decision-making module of the system is strictly defined by using the formal method to enhance the credibility of the system,finally the prototype of point monitoring unit system is built.Based on properties of the safety critical system to construct the hardware architecture,the software architecture is designed based on the verifiability of the system.Separate control flow from data flow as the logic decision-making layer of the system software,which is the object of formally models and validates.Put forward measures to ensure the reliability of the system,combined with the application scenario;The tool chain is used to build the modeling verification scheme from semiformalization to formalization.For the logic decision layer,Use the hazard analysis of Systems-Theoretic Accident Model and Processes(STAMP)to find the defects of the current system and deduce the security requirements of the system.Then complete the functional requirements according to the actual application scenarios.This provides the foundation for the establishment of meta-model.Furthermore,we instantiate security constraints and functional requirements,add details and the parameter to build metamodel.Based on the meta-model,procedure flow chart and Stateflow models of Simulink are constructed to provide templates and simulation basis for formal modeling;Customizes the B method’s and validation scheme according to the procedural properties of the model to make it simpler,more efficient and targeted in the formalized modeling and validation phase.Formalize the model according to the meta-model and Simulink Stateflow,build the invariant by security requirements,and use Pro B’s model checking function to verify the correctness of the model,then generate the target code;The last step is to add and integrate specific algorithms and build the interlocking environment,and further test and confirm the functional satisfiability of the system in the simulation environment.This thesis implements the formal development of logic decision-making layer in point monitoring unit software system.The safety critical module has been proved in Atelier B platform,and the modle can generate corresponding embedded code,which successfully integrates the code into the simulation environment to complete the simulation.It proves that this development route is suitable for defining and developing such complex logic systems,and provides reference for the development of safty critical systems.