随着嵌入式软件系统在汽车、核工业、航空等安全关键领域的广泛应用,其失效将会导致财产的损失、环境的破坏甚至人员的伤亡,使得保障软件安全性成为系统开发过程中的重要部分。此外,嵌入式软件系统规模和复杂度的增加使其多采用构件化分布式架构。因此,针对构件化嵌入式软件系统进行安全性分析已成为现代嵌入式系统安全性保障的重要方法和研究热点。而传统的安全性分析方法主要应用在软件的需求分析阶段,在软件设计阶段仍缺乏有效的安全性分析方法和工具。形式化方法是一种基于严格的数学理论为软件和硬件系统提供精确规约、分析和验证的方法。对于具有高安全性需求的嵌入式系统,建立有效的形式化分析验证技术可以为安全性分析提供支持。因此,在嵌入式软件设计阶段的安全性建模中引入形式化方法对其进行分析,得到软件安全性分析结果,可以有效提高嵌入式软件安全性。本文主要围绕构件化嵌入式软件系统设计阶段的安全性建模和分析问题展开研究。采用Sys ML和状态事件故障树建立安全性设计模型,对构件化嵌入式软件系统设计阶段模型的静态结构和动态失效行为两方面的安全性分析工作进行研究。主要工作包含以下几个方面:(1)针对构件化嵌入式软件静态结构的构件安全等级依赖问题,给出了分析构件之间安全等级依赖与安全认证目标之间一致性的方法。首先根据安全认证标准DO-178B分析软件构件安全等级依赖所必须达到的认证目标,其次采用Sys ML块定义图建立带有安全等级信息的软件静态结构的安全性设计模型。由于Sys ML块定义图缺乏严格的形式语义,建立形式化模型块依赖图对Sys ML块定义图进行形式化语义描述。在此基础上给出算法用于分析构件安全等级依赖与认证目标之间的一致性。采用该方法对嵌入式软件系统静态结构的安全等级依赖关系进行分析,能够提高系统整体的安全性,并为安全认提供证据。(2)针对构件化嵌入式软件动态失效行为因果链中的最小割序集分析问题,采用状态事件故障树建立系统的失效行为因果链。由于状态事件故障树缺乏严格的形式语义,提出形式化模型卫式接口自动机对状态事件故障树行为方面的形式化语义进行描述。在此基础上,给出卫式接口自动机的并行组合聚合框架用于生成状态事件故障树的形式化语义,并通过定义弱互模拟操作对组合过程中的状态空间进行约简。最后给出了基于该形式化语义的状态事件故障树最小割序集分析方法。分析结果可以为软件的测试用例生成以及模型检验提供支持。(3)针对构件化嵌入式系统动态失效行为的安全性参数分析问题,提出了软件失效行为的概率和时间特性分析方法。由于状态事件故障树能够同时描述构件化嵌入式系统的动态失效行为和概率特性,在状态事件故障树最小割序集分析的基础上,可进一步分析其概率时间参数。为了描述状态事件故障树带概率信息的形式化语义,提出能够同时描述功能行为和概率信息的形式化模型接口交互马尔可夫链用于描述状态事件故障树的形式化语义。在此基础上,给出接口交互马尔可夫链的并行组合聚合框架用于获得状态事件故障树的形式语义,并通过定义接口交互马尔可夫链的弱互模拟操作对组合过程中的状态空间进行约简。最后,基于该形式语义分别采用已有的概率分析工具MRMC和IMCA对状态事件故障树的概率和时间参数进行分析。分析结果可以为软件安全性评估提供支持。(4)基于上述方法,设计了一个构件化嵌入式软件安全性分析工具T-CESSA(Tool for component-based embedded software safety analysis),支持嵌入式软件静态结构的安全等级依赖分析、动态失效行为的最小割序集以及安全性参数的分析,并且通过典型嵌入式软件系统的实例分析说明上述方法的有效性。