System Safety Modeling And Analysis Methodology Based On Feature Configuration

With the development of computer technology,embedded system is more widely used in safetycritical fields such as aerospace,nuclear application,rail transportation,medical treatment and so on.How to guarantee the safety of system and prevent the catastrophic accidents caused by the system failure has become a hot spot in the field of safety and software engineering.Developing safety-critical system based on MBSA in the industry,sponsored by the European Space Agency's COMPASS project,for safety critical systems such as spacecraft systems that are modeled using SLIM,not only can describe the nominal behavior of hardware and software of system,but also describe the system probabilistic of fault and it influences on the system.SLIM language has gradually becoming the European Space Agency's standard language in the system modeling.However,the original SLIM in the modeling method of system behavior in case of failure of the real system is not accurate enough,and traditional safety analysis for SLIM model is facing big problems of fault space.For safety analysis of safety-critical systems,this thesis proposes system safety modeling and analysis methodology based on feature configuration.Feature model describes the relationship between family characteristics and variability of software product family in software product line engineering.Furthermore,software product line model checking tool SNIP is capable of checking all the products in the feature set at a time whether the specified attribute is violated.For fault space is huge in the system,the combination of features in the software product line is similar to the fault combination in the system,so the software product line feature configuration is applied to the system safety analysis.Firstly,based on feature configuration of software product line,the extended model of system is established by SLIM.We introduce that how to use SLIM to create the nominal model,fault model and fault injection.The fault injection method of the original SLIM was modified according to the feature configuration of the software product line,and the fault model of the system was established according to the feature configuration.Due to the fault model,the model of nominal and error model is associated and the SLIM extended model of the system is created.Secondly,SLIM extended model was translated into f Promela+TVL that SNIP can recognize.Through the SLIM and the analysis of semantics in f Promela+TVL,we get the rules of model SLIM translate to model f Promela+TVL and prove the correctness of translation.When we get the f Promela+TVL,and the constraint of fault is added into the TVL.Then,the LTL specification of the safety requirements is given by linear temporal logic,using the software product line model checking tool SNIP to verify the safety of the f Promela+TVL model,get the verification result.Finally,according to the system safety modeling and analysis method,this thesis design and implement the system safety modeling and analysis tool S2 F.Using the method proposed in this thesis and S2 F tool,we present a case study for the Airbus A320 hydraulic system.