● 摘要
软件安全性是指控制系统的软件不对人员、财产和环境造成危害的一种性质。为了确保航空关键系统的安全性，评估人员需要验证软件及其开发过程是否满足安全标准所提出的一系列安全目标。一种被广泛使用的安全验证手段是基于证据的安全论证。
在进行评估前，需要从软件过程制品中抽取论证目标所需的安全证据。然而，相关研究和安全评估实践表明，证据收集存在着如下问题：1）手工提取证据需求不仅耗时，且依赖于个人经验，这将降低证据的有效性和可信度；2) 软件过程产生的原始制品数据量大，结构复杂，增加了证据抽取的难度和工作量；3) 不同项目中产生的过程制品的数据格式各异，这将降低证据需求的可复用性。
针对证据收集中存在的问题，参考现有的研究，本文采用基于模型的证据收集方法，研究并提取了航空软件安全标准RTCA DO-178C的证据模型，并应用于某航空操作系统项目评估过程中的证据收集；同时开发了轻量级模型数据管理器，用于支持基于模型的证据收集。
描述安全论证过程的逻辑是安全评估的另一个主题。对自然语言描述的安全目标进行论证依赖于主观理解，这造成论证中存在潜在的逻辑二义性和不一致性。本文提出形式化的安全论证方法：通过形式逻辑命题精确地、无二义性地描述安全目标的论证逻辑。基于这一方法，我们提取了DO-178C开发和测试过程的安全目标的形式逻辑命题，并开发了相应的形式化验证工具，用于支持自动化安全论证。
本文将基于模型的证据收集与形式化的安全验证方法相结合，开发了证据驱动验证器，用于支持基于证据的自动化安全论证。最后，在工具的支持下，本文验证了某航空操作系统项目的开发和测试过程是否满足DO-178C的安全目标；通过案例分析，验证了工具的有效性以及本文提出的安全评估方法的可行性。