嵌入式系统在航空航天、核工业等各种安全关键系统中有着广泛应用。这类系统一旦发生故障将会导致严重的财产损失和人员伤亡,因此安全性极为重要。嵌入式系统具有“复杂化、系统化、普适化、多架构设计”的特点,对其进行安全性分析与验证变得愈发困难。本文主要关注飞行器嵌入式系统,对其进行安全性分析与验证存在以下方面的不足:一是安全标准中对功能研制保证等级的分配要求缺乏一致性分析验证方法;二是已有方法做故障率计算主要面向常规情况,而针对失效满足混合分布和不确定性分布等情况时面临困难;三是在分析系统故障时难以将故障原因与系统组件行为进行关联,不易实现故障状态可达性验证。针对上述问题,本文面向安全关键飞行器嵌入式系统提出安全性分析与验证的若干方法,主要内容如下:（1）针对系统静态结构的功能研制保证等级分配问题,依据安全认证标准提取组件之间功能研制保证等级（Functional Development Assurance Level,FDAL）依赖要求,据此检验嵌入式系统组件间的安全等级依赖关系与认证目标的一致性。通过扩展Sys ML块定义图对系统的静态结构建立安全性设计模型,并将其转化为块依赖图,以刻画系统组件之间的FDAL依赖关系;之后从相关安全标准中抽取有关系统FDAL认证目标;最后验证系统的FDAL依赖关系与认证目标的一致性。（2）针对系统安全风险分析,提出在两种特殊场景下基于动态故障树的定量分析方法。设计了动态故障树模型到有序二元决策图的映射方法,再通过遍历有序二元决策图得到动态故障树的最小割序集。在混合失效分布的情况,通过失效路径组合的方法得到概率计算公式,进行计算得到系统故障概率。在不确定性分布的情况,结合模糊原理,将模糊动态故障树转化为模糊马尔科夫链模型,进行计算得到系统模糊故障概率。（3）针对系统故障状态是否可达问题,基于扩展后的故障状态图提出了一种系统故障状态可达性验证方法。通过从系统故障树抽取安全需求信息,设计算法实现了从故障树和状态图到故障状态图的自动构建。将状态图映射到时间自动机,利用模型检测工具UPPAAL进行故障状态可达性验证。（4）基于上述方法,设计了适用于嵌入式系统的安全性分析工具Tool4ESSA,支持嵌入式系统的静态结构的安全等级分析、系统故障率计算、嵌入式系统故障状态可达性分析验证,并针对每个分析方法给出了具体案例对方法有效性进行了分析说明。