Research On System Requirements And Design Safety Analysis Method Based On Formal Model

Modern safety critical system(such as computer control system in aerospace,nuclear power and other fields)refers to a kind of complex system that may cause a large number of casualties,serious economic loss or environmental damage due to its failure.Therefore,in the design of such safety-critical systems,it is necessary not only to ensure the correctness of its functions,but also to analyze it at multiple levels such as requirements and design to improve the risk and fault response capabilities of the system.Traditional methods of manually analyzing requirements documents and system design are increasingly difficult to find potential requirements errors,consistency,completeness and other problems in such complex system requirements,as well as system reliability and safety analysis at the design level.MBSA(model based safety analysis)is a kind of modeling and analysis method for safety critical system requirements and design based on system abstract model.At the same time,due to the characteristics of strict mathematical model and automatic analysis algorithm of formal method,the industry has begun to apply relevant formal model and tools in recent years.How to combine the formal method with the model-based system analysis method to analyze the safety and reliability of the safety critical system is an important challenge in this field.The main work of this paper involves two levels of analysis methods based on requirements-oriented and design-oriented formal models.Modeling and analysis of safety-critical system requirements are carried out,and system failure behavior is modeled and analyzed at the design level.The specific contents include the following aspects:First of all,a system requirement modeling and analysis framework based on formal variable relationship model(VRM)is designed.The framework includes both modeling and analysis.In the aspect of modeling,it includes a requirements dictionary covering all kinds of variables,defines a formal six-tuple of the VRM model,constructs a set of topologically ordered dependencies to represent the variable relationships,distinguishes the variable relationships in different tenses.and defines different event states.In the aspect of model analysis,a set of paradigm constraints is designed to analyze the consistency and completeness of the demand model;And based on the definition of these paradigms,a set of algorithms for the paradigm compliance verification of the demand model are designed.Secondly,the MBSA-based system design modeling and model analysis methods are analyzed,including establishing models according to system specifications,designing fault modes according to system behavior characteristics,using fault injection mechanism to extend the normal behavior of the system,and finally performing system safety verification and analysis on the extended model,such as model checking to analyze system attributes,fault tree analysis,and failure mode effect analysis,a MBSA-based SLIM modeling method is proposed.Thirdly,a framework for modeling and verifying the requirement relationship model has been implemented,and a prototype tool has been constructed.The tool is capable of modeling and designing system requirements based on the VRM model,and can conduct verification and analysis of requirements' consistency,integrity and other paradigm constraints.The display interface scheduling system in the cockpit display and control system of civil aircraft is used as an example to analyze,and its related requirements are modeled and analyzed using the requirements relationship model modeling and verification framework.Finally,taking the wheel brake system of air6110 standard as an example,the fault extension and safety verification based on formalization at the system design level are carried out.It includes analyzing the structural characteristics of the wheel brake system and layering it;using slim language to build a functional model of the layered system architecture;considering the possible failure conditions and designing a series of failure modes;carrying out fault injection and safety analysis,and obtaining typical system safety analysis results,such as fault tree and FMEA table.