Research On System Safety Analysis And Verification Based On Formal Model

With the development of society,the use of safety-critical systems has been greatly improved.It is an important research content in safety-critical systems such as aerospace,nuclear power plants,and high-speed railways,that how to improve their safety and prevent human casualties and the destruction of natural resources.The design and analysis of safety-critical systems?eg,avionics systems?not only ensure that the system can perform the specified functions normally but also ensure that the system Corresponding safety protection should be given when certain components in the system fail or due to environmental or human-induced dangerous situations.First of all,the requirement specification of the safety-critical system is very important.The complete and definite requirement can effectively guide the development and realization of the system.In addition,the development of safety-critical systems must not only take their functional requirements into account,but also the possible failure behavior of their components.In response to the above problems,the main work of this paper is to design a methodological framework that can identify the needs of safety-critical systems and model and verify the failure behavior.The specific work is as follows:?1?Firstly,based on the importance of safety-critical system requirement specification,the paper introduces the RSML^-e language for the system requirement specification.RSML^-e language is a formal modeling language based on the four-variable model.The RSML^-e models can help communicate the requirements of system developers and non-developers.However,since RSML^-e language does not have the characteristics of model checking,this paper analyzes the grammatical features of the RSML^-e language and NuSMV language in detail and proposes a set of transformation rules that convert the RSML^-e language to NuSMV language.Based on the idea of this system requirement specification,model transformation,and model checking,this paper presents a set of preliminary requirement verification framework based on NuSMV model checking.?2?For the safety-critical system,to ensure the correctness of the functional behavior is only the first step in the safety analysis.What further needs to be done is to analyze the fault behavior of the system.After introducing MBSA method idea and fault injection mechanism,this paper presents a MBSA-based system verification and safety analysis framework based on the idea of fault extension and MBSA analysis and verification,which is used to perform fault injection extensions in the model of NuSMV and analyze the function safety assessments to generate fault trees and FMEA tables of extend model.?3?In this paper,a real avionics flight automation system is taken as an example to analyze.First of all,the paper describes its system architecture,and then select the appropriate subsystem?AFCS?for RSML^-e requirements modeling and model transformation,then perform model checking in the NuSMV Model.The validity and practicability of the preliminary requirement verification framework based on NuSMV model checking proposed in this paper are illustrated.Then injects the fault into the model and customizes the Outputdisorder fault mode according to the characteristics of AFCS system during the process of fault injection.The extended model is successfully generated.Based on the extended model,the fault tree and FMEA table are automatically generated using the xSAP tool.