基于SCADE的FADEC軟件通用基準模型庫開發(fā)

周彰毅，張 春，朱理化，黃 浩，李紀波

（中國航發(fā)控制系統(tǒng)研究所，江蘇無錫 214063）

0 引言

航空發(fā)動機全權限數(shù)字電子控制（Full Authority Digital Electronic Control，F(xiàn)ADEC）系統(tǒng)控制軟件是實現(xiàn)航空發(fā)動機控制系統(tǒng)功能和控制品質的關鍵環(huán)節(jié)，是FADEC系統(tǒng)所有部件中最為關鍵和重要的部件。根據(jù)DO-178C中軟件安全等級定義，F(xiàn)ADEC軟件的安全等級為最高等的A級。FADEC軟件開發(fā)的難度大、周期長、成本高，而且由于需求變更頻繁、功能不斷綜合和安全性要求日益嚴苛等原因，控制軟件開發(fā)面臨的挑戰(zhàn)越來越嚴峻。傳統(tǒng)手工編碼的軟件開發(fā)模式在提高軟件質量和研制效率方面的局限性越來越明顯。基于模型的開發(fā)（Model-Based Development，MBD）具有圖形化設計、自動代碼生成和早期驗證等優(yōu)勢，可以在設計階段提前發(fā)現(xiàn)軟件缺陷并進行封閉，使用經鑒定的代碼生成器可以省去編碼、代碼審查和單元測試，使得開發(fā)人員能把更多精力集中于軟件設計和控制算法優(yōu)化。安全關鍵軟件開發(fā)環(huán)境（Safety Critical Application Development Environment，SCADE）是1款專注于安全關鍵系統(tǒng)和軟件開發(fā)集成開發(fā)環(huán)境的軟件，提供一整套MBD解決方案，包含多個經適航鑒定的工具箱，在A380飛機、LEAP系列發(fā)動機等應用的眾多航空機載軟件都使用SCADE開發(fā)并通過適航認證。

李夏研究發(fā)現(xiàn)軟件重用是提高軟件研發(fā)效率的重要手段，能減少重復開發(fā)，提高軟件可靠性和可維修性，并有助于軟件設計的標準化和設計風格統(tǒng)一，進而提高系統(tǒng)間的互操作性；Frakes等提出軟件重用資產包括軟件本身和軟件領域知識，軟件重用的目的是提升軟件質量和效率，可重用性是軟件質量的重要考量因素，同時提出可重用的測量方法，并闡述了領域工程在軟件重用中的重要作用；Mika等分析了基于IEC 61499功能模塊建模和編程標準，并識別和提出基于該標準的多種軟件可配置和可重用策略。在基于模型的軟件開發(fā)中，基于領域知識提取通用算法和功能，構建可重用基準模型庫，形成1套可重用的庫需求、庫模型和庫驗證用例等組織資產，已成為提升軟件研制能力的共識。

本文分析了DO-331中關于可重用構建和模型庫相關的標準和指南，結合航空發(fā)動機FADEC軟件的領域特點和工程需要，進行自定義基準模型庫的研制。

1 模型庫的相關標準和要求分析

在基于模型軟件的軟件開發(fā)中，通用軟件需求的提取和自定義模型庫的研制是基礎性工作，因此，模型庫基于模型開發(fā)和驗證的核心，用于建模、驗證、編碼和測試。此外，不同研制階段的模型包含的要素和內容不盡相同，采用模型庫管理的方法是實現(xiàn)仿真模型重用系統(tǒng)化和工程化的必須和必然。

1.1 模型庫的開發(fā)和使用的基本原則

針對DO-178C和DO-278A的“基于模型開發(fā)和驗證的補充”（即DO-331標準）對模型庫的開發(fā)和使用做了專題討論，明確規(guī)定了模型庫的開發(fā)和使用的基本原則：

（1）在DO-178C/DO-278A關于安全等級及其目標符合性方面，模型庫的開發(fā)和驗證過程的活動及目標應與使用該模型庫的軟件一致；

（2）模型庫使用方和適航認證當局要能獲得DO-178C/DO-278A中相應軟件安全等級要求的關于模型生命周期過程的所有數(shù)據(jù)；

（3）模型庫開發(fā)方要提供關于模型庫的相關文檔；

（4）模型庫使用方應提供模型庫的操作需求（若模型庫的開發(fā)方和使用方相同，則操作需求可以包含在模型庫需求中）。

1.2 模型庫的需求

模型庫的開發(fā)首先要進行模型庫的需求分析，模型庫可能的使用場景很多，因此要清晰地描述模型庫可能的使用條件，其衍生需求應在文檔中清晰描述并提供給模型庫的使用方，模型庫的需求應該包括：接口約定；輸入約束，比如數(shù)據(jù)的限制；內存管理；調度條件；系統(tǒng)資源標識；其他限制。

1.3 模型庫的驗證目標

在模型庫的驗證方面，模型庫的使用方應提供證明材料，證明模型庫開發(fā)方和使用模型庫的軟件開發(fā)方所完成的活動能共同滿足模型庫和軟件應滿足的目標。模型庫的驗證目標應至少包括（見DO-331表MB.6）：

（1）驗證模型庫是否符合其需求；

（2）審查模型庫在軟件中的使用情況；

（3）對使用模型的軟件和模型庫進行集成測試。

1.4 定義模型庫規(guī)范和配置管理

應定義模型庫規(guī)范，其內容主要包括開發(fā)、驗證和使用規(guī)范。模型庫的建模/設計規(guī)范應提供給模型的使用方，內容包括模型庫內部設計/編碼規(guī)則，模型庫與MBD環(huán)境和代碼的接合規(guī)則。模型庫的使用方應驗證模型庫開發(fā)所用的設計/編碼規(guī)則與使用該庫的軟件開發(fā)所用的設計/編碼規(guī)則是否兼容。

在配置管理方面，模型庫開發(fā)和驗證過程的配置管理級別應與使用該模型庫的軟件的配置管理級別相一致。

2 模型庫設計和驗證

2.1 三角函數(shù)類

在軟件開發(fā)中，對于三角函數(shù)或者反三角函數(shù)，通常使用編譯器自帶的實現(xiàn)函數(shù)或者第三方代碼庫，不太關注其具體實現(xiàn)方法。但航空發(fā)動機控制軟件對時間資源、空間資源和安全性都有很高的要求，開發(fā)人員往往會重新開發(fā)而不是使用自帶的三角函數(shù)，本節(jié)以正弦模型的開發(fā)為例進行分析，其他三角函數(shù)模型的設計與此類似。

根據(jù)泰勒定理，在任何包含和的區(qū)間上，如果1個函數(shù)及其前+1階導數(shù)都是連續(xù)的，那么該函數(shù)在處的值可以表示為

式中：余項R 定義為

式中：為積分變量。

該定理表明：任何光滑的函數(shù)都可以用多項式來逼近它。

對于正弦函數(shù)sin，將其在原點（=0）進行泰勒展開，經過求導計算后，得到泰勒多項式為

式中：的單位為弧度。

正弦函數(shù)SCADE模型如圖1所示。模型的輸入為任何角度，輸出為正弦值。首先將任意輸入角度Angle轉換到[-360°，360°]，得到Angle_Limited1，然后將Angle_Limited1轉換到[-90°，90°]，得到Angle_Limited2，再換算到[-π/2，π/2]范圍內的弧度值，最后進行多項式計算，得到正弦值Sin。

采用SCADE模型計算與理論計算對比的方式進行正弦函數(shù)模型的驗證，得到的對比曲線如圖2所示。因正弦函數(shù)是周期函數(shù)，僅顯示了[-360°，360°]范圍的計算結果。從圖中可見，SCADE模型計算值和理論計算值幾乎一致。

圖1 正弦函數(shù)SCADE模型

圖2 正弦函數(shù)SCADE模型和理論計算對比驗證

2.2 求根類

對于方程()=0的求解，根據(jù)牛頓-瑞普遜方法，如圖3所示。如果根的初始值是x ，則可以在[x ,(x )]處繪制1條與函數(shù)相切的切線，該切線與軸的交點x 表示根的新的估計值。

圖3 牛頓-瑞普遜法

牛頓-瑞普遜法可以根據(jù)幾何表示來推導，在圖3中，在x 處的1階導數(shù)等于斜率

將式（4）變形得到

式（5）稱為牛頓-瑞普遜公式，通過多次迭代，x 不斷接近方程()=0的真正解，在工程中通常采用誤差項作為收斂判斷和終止迭代的條件，當前迭代結果的誤差為

當?shù)恼`差在預先設定的可接受容限內，則停止迭代，即

圖4 開平方根SCADE模型

根據(jù)DO-178C和DO-331標準對軟件A級安全關鍵軟件的測試要求，從正常測試（包括有效等價類和邊界內的值）和魯棒性測試（包括無效等價類、邊界上和邊界外的值）2方面考慮，通過等價類劃分、邊界值分析和重復性考慮等設計開平方根的測試用例，編寫模型測試腳本，在SCADE的合格測試環(huán)境（Qualified Test Environment，QTE）中進行模型測試，對應的測試用例和結果見表1。從表中可見，開平方根模型在正常值和非正常值情況下均符合需求。

表1 開平方根模型測試用例和測試結果

2.3 濾波算法類

在航空發(fā)動機FADEC系統(tǒng)中，在高溫高壓條件下對熱端部件的信號采集存在較大的外界干擾，為削弱這些外界擾動對控制品質的影響，通常需要對信號進行濾理，其中，超前滯后濾波是一種高效實用的濾波方法。超前滯后環(huán)節(jié)是非線性的超前滯后函數(shù)，在動態(tài)下，超前滯后環(huán)節(jié)的輸出值是舊輸入、舊輸出、新輸入、超前和滯后時間常數(shù)的函數(shù)。超前滯后濾波在域的傳遞函數(shù)為

式中：為超前時間常數(shù)；為滯后時間常數(shù)；為濾波輸入信號；為濾波輸出信號。

該傳遞函數(shù)可以表示為

式中：()為微分環(huán)節(jié)，其特性為超前；()為1階慣性環(huán)節(jié)，其特性滯后延遲。

SCADE僅適用于離散系統(tǒng)的控制系統(tǒng)和軟件設計，不支持連續(xù)域的建模，因此需從域轉換為域。根據(jù)經典控制理論中的變換理論，采用雙線性變換的方法對式（8）進行轉換，得到域的傳遞函數(shù)

進一步得到對應的差分方程

依據(jù)差分方程，在SCADE中完成超前滯后校正模型的設計，如圖5所示。

圖5 超前滯后校正模型的設計

對于該濾波算法的驗證，采用模型封裝技術將SCADE模型封裝成Simulink模型，導入到Matlab/Simulink環(huán)境中，在相同濾波參數(shù)配置情況下，將封裝后的SCADE濾波器模型與Simulink自帶的超前滯后校正模型進行對比仿真，如圖6所示。以某溫度信號作為濾波原始信號進行濾波，如圖7所示。從圖中可見，設計的濾波器模型有較好的濾波效果。

圖6 超前滯后模型對比仿真

圖7 超前滯后模型仿真結果對比

2.4 余度算法類

出于對安全關鍵系統(tǒng)的安全性和可靠性考慮，F(xiàn)ADEC控制系統(tǒng)中常采用余度技術，如關鍵信號的采集和處理常用二余度和三余度。本節(jié)以二余度模擬量信號表決算法為例進行模型設計，并使用SCADE Verifier對這類條件組合模型進行形式化驗證。

記輸入信號（X1，X1_Valid）、（X2，X2_Valid）分別為傳感器A、B的信號值與有效性，若X1_Valid=True，則表示X1無故障，該信號可用，X2同理。輸出信號為（X，X_Faut Info），X為表決后的模擬量，X_FautInfo為表決后的故障綜合信息，根據(jù)獲取的雙通道信號是否有效及信號值得到如下高層需求：

R1：若雙通道信號均有效，且信號偏差未超過容許閾值（Threshold），則表決值為和的平均值，表決故障信息置為信號完好，即X_Faut Info=Signal_OK；

R2：若雙通道信號均有效，且信號偏差超過容許閾值，此時無法判斷哪個傳感器的信號有效，表決值為安全值（X_Safe），表決故障信息置為表決故障（VoteFault）；

R3：若僅1個通道信號有效，則表決值使用該有效信號值，表決故障信息置為信號完好；

R4：若雙通道信號均無效，則表決值使用默認值（X_Default），表決故障信息置為信號故障（Signal-Fault）；

其中X_Default和X_Safe可能是1個常數(shù)，或者是保持輸出的前值，與具體信號特性相關。

使用SCADE真值表進行模型設計，對應的二余度表決SCADE模型如圖8所示。

圖8 二余度表決SCADE模型

對于余度表決算法這類條件組合模型，除了采用常規(guī)的正向模型測試方法外，還采用了形式化方法，基于窮盡搜索對各種場景進行分析驗證。SCADE的底層支持語言是形式化的同步語言Lustre，且提供了形式化驗證工具Design Verifier，使 用SCADE進行形式化驗證的一般步驟如圖9所示。

圖9 使用SCADE進行形式化驗證的一般步驟

本例使用分支時態(tài)邏輯（Computation Tree Logic，CTL）將高層需求提取為待驗證的安全屬性。對需求R1、R2、R3、R4的安全屬性進行描述，其中R1的安全屬性可描述為

→=(1+2)/2∧Fault Info=Signal)（14）式中：AG表示對于所有狀態(tài)；∧表示邏輯與；→為邏輯蘊含符；為表決值；FaultInfo為表決信息。

對需求R1，根據(jù)安全屬性可知，當1_為真，2_為真，且2個傳感器值偏差在容許閾值范圍內時，表決值應等于平均值，將這個判斷結果賦給布爾變量Prop_R1_1（圖9），且此時信號故障信息應為完好，將這個判斷結果賦給布爾變量Prop_R1_2。Implies為SCADE驗證庫中的邏輯蘊含運算符，需求R1的驗證模型如圖10所示。Prop_R1_1、Prop_R1_2即為形式化驗證的分析對象。

圖10 需求R1的驗證模型

以某溫度信號的表決作為分析對象，采用SCADE Verifier執(zhí)行驗證模型進行形式化自動分析，分析結果見表2。從表中可見，設計結果正確，沒有存在反例。

表2 R1形式化分析結果

對R2、R3和R4可做類似分析。

3 結束語

MBD是應對FADEC軟件面臨挑戰(zhàn)的一種有效途徑，可重用基準模型庫是MBD的基礎和關鍵部件，對降低項目的研發(fā)成本、提升項目的效率和質量、縮短研制周期具有十分重要的作用。本文探討了模型庫開發(fā)的標準和要求，立足航空發(fā)動機控制的切實需要，提取FADEC軟件通用要求，并基于SCADE開發(fā)環(huán)境進行模型庫開發(fā)，從數(shù)理分析、模型設計和模型驗證幾個維度闡述了基準模型庫開發(fā)方法和過程。該基準模型庫已通過了專業(yè)測試團隊的測試，并已經應用在多個FADEC軟件項目中，其正確性和可靠性已在各階段的工程試驗中得以檢驗。