论文部分内容阅读
现代电子机载系统正由电子机械密集型向软件密集型转变,系统功能的实现越来越依赖于软件,导致软件的安全性对系统的安全至关重要。软件测试是开发过程中用来验证软件功能正确性的方法。然而,软件功能的正确性不能保证安全关键系统的安全运行。软件必须根据安全分析确定的安全需求进行验证并且需要识别出预期以外的功能,以确保识别出的潜在危险行为不会发生。软件的复杂性使得用传统的安全性分析方法定义适当的软件安全性需求变得困难。系统理论过程分析(System Theoretic Process Analysis,STPA)是一种基于系统理论事故模型和过程(Systems Theoretic Accident Model and Processes,STAMP)的安全性分析方法,用于识别系统危害,包括与软件相关的危害,但是该方法严重依赖分析人员经验。此外,目前在实际工程中采用基于模型的软件开发方式成为趋势。为此,本文以模型为核心,提出一种基于形式化扩展STPA方法和RTCA DO-331适航标准相结合的机载软件模型验证方法。本文的主要研究工作及创新点如下:(1)本文首先采用安全关键应用开发环境(Safety Critical Application Development Environment,SCADE)开发无人机中的安全关键软件,确保软件的无二义性。根据固定翼无人机数学模型在SCADE中建立闭环仿真环境,实现对软件的功能仿真,完成软件功能验证。(2)为了提高软件的安全性,本文提出一种基于形式化扩展的STPA方法捕获软件安全性需求并形成形式化规范,结合模型检验技术对软件进行安全性验证的方法。该方法从系统规范出发,确定系统软件失效可能导致的系统级事故与危险,并构建软件安全控制结构,识别软件中的危险行为。基于已确定的潜在危险行为,结合构建的软件过程模型进行进一步细化分析,确定每个潜在危险行为发生的原因,并转化为相应的软件安全性需求,然后形成规约模型,借助模型检验技术,完成对软件的安全性验证。(3)在机载电子设备领域,为了保证机载电子设备的软件安全性,需要基于机载软件的适航标准进行符合性验证。本文为了进一步提高安全关键软件的安全性,对RTCA DO-331中模型覆盖率和代码覆盖率等适航目标采用基于需求的测试覆盖方法进行了验证,保证安全关键软件未执行预期以外的功能。