Research On System Requirements Modeling And Safety Analysis Based On Formal Method

With the birth and rapid development of computers,they have been widely used in various industries and fields.The application of the computer plays an important role in safety-critical systems.For safety-critical systems,system incidental failures of the computer often result in huge loss of life and property.Therefore,it is essential to analyze the safety of safety-critical systems,such as aircraft airborne systems.It is not only necessary to ensure that the normal functional behavior of the system is complete,but also to ensure that the possible system functional failure effects can be considered adequately and the system can respond to failures in time.Formal method is a kind of mathematical modeling and analysis method based on logical formal language.It can be used to model,analyze and verify safety-critical systems and improve the safety of those systems.Aiming at the safety of aviation safety-critical system requirements,this thesis develops a system requirements modeling and analysis based on formal methods,including the following aspects:(1)Designing a requirements-oriented modeling and safety analysis framework based on a four-variable model.This framework analyzes the system based on the four-variable model according to the importance of the safety-critical system requirements specification,models the system by the formal table language SCR,and verifies the requirements of the SCR model.This thesis applies the whole ideas to the model the flight guidance system and analyzes the integrity of the requirements.Besides,it proposes a requirements verification framework based on NuSMV according to the thought of system requirements specification,model transformation and model checking.Finally,it can analyze the system according to failure behaviors based on MBSA.(2)Proposing a transformation method for transforming SCR models into NuSMV models.Since the SCR model based on the four-variable model can only verify the completeness of the system requirements,it can not check the system functional properties.So the SCR model needs to be transformed into a NuSMV model that can check functional properties.This thesis studies the grammatical semantics and characteristics of SCR language and NuSMV language and proposes a model transformation method between two languages,which can guarantee semantic consistency.The method includes the transformation of types and variables,the correspondence between tenses and the transformation of modes and terms in SCR language and sub-modules in NuSMV language.(3)Establishing a system verification and safety analysis process based on the fault injectionmechanism and model expansion.The process includes designing system failure behavior according to system behavior characteristics,injecting fault events into system normal behavior model,identifying system top events,extending system normal behavior model to obtain the failure model based on model extension and performing fault analysis,such as generating fault tree and FMEA table.(4)Carrying out a case analysis based on an actual integrated avionics system which models the system requirements and analyzes the safety.The example includes analyzing the structure of the flight guidance system and the mode logic it contains,carrying out system requirements analysis,using SCR language to model the system,transforming the SCR model to a NuSMV model which can be used to check the system functional properties and designing failure behavior to perform fault analysis,such as generating fault tree and FMEA table.