中文摘要：

目前,能够对航空航天、核电等领域中复杂嵌入式系统安全关键软件功能建模和故障分析的方法尚未得到统一;致使功能模型分析中缺乏安全属性来源,故障分析得到的危害无法在功能设计中得到避免.状态事件故障树是一种适合描述复杂系统中功能失效因果关系的建模技术,统一了功能建模和故障分析;但是,由于其缺乏精确语义,难以直接进行软件的安全性分析.为此,提出一种基于状态事件故障树的软件安全性分析方法：首先,通过元素映射以及逻辑门转换,将状态事件故障树扩展为附加故障语义信息的故障状态机;然后,将故障状态机转换到时间自动机;最后,在模型检测工具UPPAAL下进行安全性测试反例分析.本文使用燃气灶控制系统的实例进行分析.

英文摘要：

Nowadays, functional modeling and fault analysis are separated for safety-critical software in complex embedded system, inthe areas of aeronautics and astronautics, nuclear power and others. It leads to the problem that functional model analysis is lack ofsafety property and the hazard getting from fault tree analysis can＇t be avoided during functional design. State/Event fault Tree（SEFT） is a modeling technique for describing the causal relations which lead to functional failure in complex systems, it can unifyfunctional modeling and fault analysis;but because of the lack of semantic precision, it can hardly be used directly for software safetyanalysis. A method for software safety analysis based on SEFF is presented in this paper. Firstly, translate SEFT to state machine addi-tion with fault semantic messages by means of mapping elements together with translating logic gates ; after which, translate state ma-chine to timed automata;at last, test software safety to collect counter-examples for analysis using model checker UPPAAL. A casestudy of gas burner control system is given in this paper.