周彰毅，张 春，朱理化，黄 浩，李纪波

（中国航发控制系统研究所，江苏无锡 214063）

0 引言

航空发动机全权限数字电子控制（Full Authority Digital Electronic Control，FADEC）系统控制软件是实现航空发动机控制系统功能和控制品质的关键环节，是FADEC系统所有部件中最为关键和重要的部件。根据DO-178C中软件安全等级定义，FADEC软件的安全等级为最高等的A级。FADEC软件开发的难度大、周期长、成本高，而且由于需求变更频繁、功能不断综合和安全性要求日益严苛等原因，控制软件开发面临的挑战越来越严峻。传统手工编码的软件开发模式在提高软件质量和研制效率方面的局限性越来越明显。基于模型的开发（Model-Based Development，MBD）具有图形化设计、自动代码生成和早期验证等优势，可以在设计阶段提前发现软件缺陷并进行封闭，使用经鉴定的代码生成器可以省去编码、代码审查和单元测试，使得开发人员能把更多精力集中于软件设计和控制算法优化。安全关键软件开发环境（Safety Critical Application Development Environment，SCADE）是1款专注于安全关键系统和软件开发集成开发环境的软件，提供一整套MBD解决方案，包含多个经适航鉴定的工具箱，在A380飞机、LEAP系列发动机等应用的众多航空机载软件都使用SCADE开发并通过适航认证。

李夏研究发现软件重用是提高软件研发效率的重要手段，能减少重复开发，提高软件可靠性和可维修性，并有助于软件设计的标准化和设计风格统一，进而提高系统间的互操作性；Frakes等提出软件重用资产包括软件本身和软件领域知识，软件重用的目的是提升软件质量和效率，可重用性是软件质量的重要考量因素，同时提出可重用的测量方法，并阐述了领域工程在软件重用中的重要作用；Mika等分析了基于IEC 61499功能模块建模和编程标准，并识别和提出基于该标准的多种软件可配置和可重用策略。在基于模型的软件开发中，基于领域知识提取通用算法和功能，构建可重用基准模型库，形成1套可重用的库需求、库模型和库验证用例等组织资产，已成为提升软件研制能力的共识。

本文分析了DO-331中关于可重用构建和模型库相关的标准和指南，结合航空发动机FADEC软件的领域特点和工程需要，进行自定义基准模型库的研制。

1 模型库的相关标准和要求分析

在基于模型软件的软件开发中，通用软件需求的提取和自定义模型库的研制是基础性工作，因此，模型库基于模型开发和验证的核心，用于建模、验证、编码和测试。此外，不同研制阶段的模型包含的要素和内容不尽相同，采用模型库管理的方法是实现仿真模型重用系统化和工程化的必须和必然。

1.1 模型库的开发和使用的基本原则

针对DO-178C和DO-278A的“基于模型开发和验证的补充”（即DO-331标准）对模型库的开发和使用做了专题讨论，明确规定了模型库的开发和使用的基本原则：

（1）在DO-178C/DO-278A关于安全等级及其目标符合性方面，模型库的开发和验证过程的活动及目标应与使用该模型库的软件一致；

（2）模型库使用方和适航认证当局要能获得DO-178C/DO-278A中相应软件安全等级要求的关于模型生命周期过程的所有数据；

（3）模型库开发方要提供关于模型库的相关文档；

（4）模型库使用方应提供模型库的操作需求（若模型库的开发方和使用方相同，则操作需求可以包含在模型库需求中）。

1.2 模型库的需求

模型库的开发首先要进行模型库的需求分析，模型库可能的使用场景很多，因此要清晰地描述模型库可能的使用条件，其衍生需求应在文档中清晰描述并提供给模型库的使用方，模型库的需求应该包括：接口约定；输入约束，比如数据的限制；内存管理；调度条件；系统资源标识；其他限制。

1.3 模型库的验证目标

在模型库的验证方面，模型库的使用方应提供证明材料，证明模型库开发方和使用模型库的软件开发方所完成的活动能共同满足模型库和软件应满足的目标。模型库的验证目标应至少包括（见DO-331表MB.6）：

（1）验证模型库是否符合其需求；

（2）审查模型库在软件中的使用情况；

（3）对使用模型的软件和模型库进行集成测试。

1.4 定义模型库规范和配置管理

应定义模型库规范，其内容主要包括开发、验证和使用规范。模型库的建模/设计规范应提供给模型的使用方，内容包括模型库内部设计/编码规则，模型库与MBD环境和代码的接合规则。模型库的使用方应验证模型库开发所用的设计/编码规则与使用该库的软件开发所用的设计/编码规则是否兼容。

在配置管理方面，模型库开发和验证过程的配置管理级别应与使用该模型库的软件的配置管理级别相一致。

2 模型库设计和验证

2.1 三角函数类

在软件开发中，对于三角函数或者反三角函数，通常使用编译器自带的实现函数或者第三方代码库，不太关注其具体实现方法。但航空发动机控制软件对时间资源、空间资源和安全性都有很高的要求，开发人员往往会重新开发而不是使用自带的三角函数，本节以正弦模型的开发为例进行分析，其他三角函数模型的设计与此类似。

根据泰勒定理，在任何包含和的区间上，如果1个函数及其前+1阶导数都是连续的，那么该函数在处的值可以表示为

式中：余项R 定义为

式中：为积分变量。

该定理表明：任何光滑的函数都可以用多项式来逼近它。

对于正弦函数sin，将其在原点（=0）进行泰勒展开，经过求导计算后，得到泰勒多项式为

式中：的单位为弧度。

正弦函数SCADE模型如图1所示。模型的输入为任何角度，输出为正弦值。首先将任意输入角度Angle转换到[-360°，360°]，得到Angle_Limited1，然后将Angle_Limited1转换到[-90°，90°]，得到Angle_Limited2，再换算到[-π/2，π/2]范围内的弧度值，最后进行多项式计算，得到正弦值Sin。

采用SCADE模型计算与理论计算对比的方式进行正弦函数模型的验证，得到的对比曲线如图2所示。因正弦函数是周期函数，仅显示了[-360°，360°]范围的计算结果。从图中可见，SCADE模型计算值和理论计算值几乎一致。

图1 正弦函数SCADE模型

图2 正弦函数SCADE模型和理论计算对比验证

2.2 求根类

对于方程()=0的求解，根据牛顿-瑞普逊方法，如图3所示。如果根的初始值是x ，则可以在[x ,(x )]处绘制1条与函数相切的切线，该切线与轴的交点x 表示根的新的估计值。

图3 牛顿-瑞普逊法

牛顿-瑞普逊法可以根据几何表示来推导，在图3中，在x 处的1阶导数等于斜率

将式（4）变形得到

式（5）称为牛顿-瑞普逊公式，通过多次迭代，x 不断接近方程()=0的真正解，在工程中通常采用误差项作为收敛判断和终止迭代的条件，当前迭代结果的误差为

当迭代的误差在预先设定的可接受容限内，则停止迭代，即

图4 开平方根SCADE模型

根据DO-178C和DO-331标准对软件A级安全关键软件的测试要求，从正常测试（包括有效等价类和边界内的值）和鲁棒性测试（包括无效等价类、边界上和边界外的值）2方面考虑，通过等价类划分、边界值分析和重复性考虑等设计开平方根的测试用例，编写模型测试脚本，在SCADE的合格测试环境（Qualified Test Environment，QTE）中进行模型测试，对应的测试用例和结果见表1。从表中可见，开平方根模型在正常值和非正常值情况下均符合需求。

表1 开平方根模型测试用例和测试结果

2.3 滤波算法类

在航空发动机FADEC系统中，在高温高压条件下对热端部件的信号采集存在较大的外界干扰，为削弱这些外界扰动对控制品质的影响，通常需要对信号进行滤理，其中，超前滞后滤波是一种高效实用的滤波方法。超前滞后环节是非线性的超前滞后函数，在动态下，超前滞后环节的输出值是旧输入、旧输出、新输入、超前和滞后时间常数的函数。超前滞后滤波在域的传递函数为

式中：为超前时间常数；为滞后时间常数；为滤波输入信号；为滤波输出信号。

该传递函数可以表示为

式中：()为微分环节，其特性为超前；()为1阶惯性环节，其特性滞后延迟。

SCADE仅适用于离散系统的控制系统和软件设计，不支持连续域的建模，因此需从域转换为域。根据经典控制理论中的变换理论，采用双线性变换的方法对式（8）进行转换，得到域的传递函数

进一步得到对应的差分方程

依据差分方程，在SCADE中完成超前滞后校正模型的设计，如图5所示。

图5 超前滞后校正模型的设计

对于该滤波算法的验证，采用模型封装技术将SCADE模型封装成Simulink模型，导入到Matlab/Simulink环境中，在相同滤波参数配置情况下，将封装后的SCADE滤波器模型与Simulink自带的超前滞后校正模型进行对比仿真，如图6所示。以某温度信号作为滤波原始信号进行滤波，如图7所示。从图中可见，设计的滤波器模型有较好的滤波效果。

图6 超前滞后模型对比仿真

图7 超前滞后模型仿真结果对比

2.4 余度算法类

出于对安全关键系统的安全性和可靠性考虑，FADEC控制系统中常采用余度技术，如关键信号的采集和处理常用二余度和三余度。本节以二余度模拟量信号表决算法为例进行模型设计，并使用SCADE Verifier对这类条件组合模型进行形式化验证。

记输入信号（X1，X1_Valid）、（X2，X2_Valid）分别为传感器A、B的信号值与有效性，若X1_Valid=True，则表示X1无故障，该信号可用，X2同理。输出信号为（X，X_Faut Info），X为表决后的模拟量，X_FautInfo为表决后的故障综合信息，根据获取的双通道信号是否有效及信号值得到如下高层需求：

R1：若双通道信号均有效，且信号偏差未超过容许阈值（Threshold），则表决值为和的平均值，表决故障信息置为信号完好，即X_Faut Info=Signal_OK；

R2：若双通道信号均有效，且信号偏差超过容许阈值，此时无法判断哪个传感器的信号有效，表决值为安全值（X_Safe），表决故障信息置为表决故障（VoteFault）；

R3：若仅1个通道信号有效，则表决值使用该有效信号值，表决故障信息置为信号完好；

R4：若双通道信号均无效，则表决值使用默认值（X_Default），表决故障信息置为信号故障（Signal-Fault）；

其中X_Default和X_Safe可能是1个常数，或者是保持输出的前值，与具体信号特性相关。

使用SCADE真值表进行模型设计，对应的二余度表决SCADE模型如图8所示。

图8 二余度表决SCADE模型

对于余度表决算法这类条件组合模型，除了采用常规的正向模型测试方法外，还采用了形式化方法，基于穷尽搜索对各种场景进行分析验证。SCADE的底层支持语言是形式化的同步语言Lustre，且提供了形式化验证工具Design Verifier，使 用SCADE进行形式化验证的一般步骤如图9所示。

图9 使用SCADE进行形式化验证的一般步骤

本例使用分支时态逻辑（Computation Tree Logic，CTL）将高层需求提取为待验证的安全属性。对需求R1、R2、R3、R4的安全属性进行描述，其中R1的安全属性可描述为

→=(1+2)/2∧Fault Info=Signal)（14）式中：AG表示对于所有状态；∧表示逻辑与；→为逻辑蕴含符；为表决值；FaultInfo为表决信息。

对需求R1，根据安全属性可知，当1_为真，2_为真，且2个传感器值偏差在容许阈值范围内时，表决值应等于平均值，将这个判断结果赋给布尔变量Prop_R1_1（图9），且此时信号故障信息应为完好，将这个判断结果赋给布尔变量Prop_R1_2。Implies为SCADE验证库中的逻辑蕴含运算符，需求R1的验证模型如图10所示。Prop_R1_1、Prop_R1_2即为形式化验证的分析对象。

图10 需求R1的验证模型

以某温度信号的表决作为分析对象，采用SCADE Verifier执行验证模型进行形式化自动分析，分析结果见表2。从表中可见，设计结果正确，没有存在反例。

表2 R1形式化分析结果

对R2、R3和R4可做类似分析。

3 结束语

MBD是应对FADEC软件面临挑战的一种有效途径，可重用基准模型库是MBD的基础和关键部件，对降低项目的研发成本、提升项目的效率和质量、缩短研制周期具有十分重要的作用。本文探讨了模型库开发的标准和要求，立足航空发动机控制的切实需要，提取FADEC软件通用要求，并基于SCADE开发环境进行模型库开发，从数理分析、模型设计和模型验证几个维度阐述了基准模型库开发方法和过程。该基准模型库已通过了专业测试团队的测试，并已经应用在多个FADEC软件项目中，其正确性和可靠性已在各阶段的工程试验中得以检验。