Safety Analysis And Research Of High Dependable System Based On Model Checking

During the entire life cycle of high-dependable system software,unpredictable losses may occur due to some minor vulnerabilities in system requirements analysis,software design,code implementation,and operation and maintenance.Therefore,in the system design and development,before putting into use,it is necessary to formally describe the attributes of the system,abstract the system software,eliminate the insignificant process,formally model the key processes,and then form the form.The model is tested to verify that the system features are effectively implemented and safe and stable,thus ensuring the integrity of the system functions.Model checking a technique that uses mathematical methods for automated verification.It is applied in many fields,and its algorithmic ideas are constantly being expanded.This study is based on model checking,using UPPAAL and other model checking tools for modeling and attribute verification,and analyzing the safety of high-dependable systems.Computer systems that have stringent requirements for system safety include not only discrete behaviors,but also time-constrained continuous behavior.In the development and modeling of such real-time systems,the current mainstream approach is to model with the semi-formal modeling language UML and time automata.The main work of this paper has the following parts:(1)Research on the basic principle and related methods of model checking,and carry out in-depth study on the time automaton model.According to the semi-formal description of the system scene,the transformation between UML time series and time automata model is studied.(2)In-depth study on the functional structure of the model checking tool UPPAAL,the syntax and semantics of the input model,and the use of tools,lay the foundation for the formal modeling and safety verification analysis of real-time high-dependable systems.(3)The related structure of the train control center in the operation scene of CTCS-3train control system in China is studied.The scene is analyzed in depth,and the UBC sequence diagram is used to describe the RBC switching scenario of the CTCS-3 train control system.UML timing diagram to time automaton transformation idea,UML time series diagram into time automaton model,using model checking tool UPPAAL to analyze and verify the safety of the column control system operation scenario.(4)In order to ensure the full safety of the high-confidence system,it is necessary to study whether the functional behavior of the system under normal conditions meets the safety requirements of the system,and also to study the system with a single fault and multiple fault combinations.System safety protection and troubleshooting capabilities.In view of this,a multi-fault based model checking safety analysis method is proposed and applied to the safety analysis and verification practice of the railway station interlocking system,which solves the multi-fault injection problem and the formal safety specification in the system safety analysis.The problem is generated,the analysis method of system function safety is expanded,and the analysis quality of system model safety is comprehensively improved.The research results of this paper can provide good theoretical guidance and technical support for the development of high-reliability system software,system safety analysis and verification,and system safety assessment.It is high-speed railway,defense weapon equipment,aerospace and other high-tech System safety in the field of dependable has a wide range of applications.