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

周彰毅，張 春，朱理化，黃 浩，李紀(jì)波

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

0 引言

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

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

本文分析了DO-331中關(guān)于可重用構(gòu)建和模型庫相關(guān)的標(biāo)準(zhǔn)和指南，結(jié)合航空發(fā)動機(jī)FADEC軟件的領(lǐng)域特點(diǎn)和工程需要，進(jìn)行自定義基準(zhǔn)模型庫的研制。

1 模型庫的相關(guān)標(biāo)準(zhǔn)和要求分析

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

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

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

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

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

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

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

1.2 模型庫的需求

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

1.3 模型庫的驗(yàn)證目標(biāo)

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

（1）驗(yàn)證模型庫是否符合其需求；

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

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

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

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

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

2 模型庫設(shè)計(jì)和驗(yàn)證

2.1 三角函數(shù)類

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

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

式中：余項(xiàng)R 定義為

式中：為積分變量。

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

對于正弦函數(shù)sin，將其在原點(diǎn)（=0）進(jìn)行泰勒展開，經(jīng)過求導(dǎo)計(jì)算后，得到泰勒多項(xiàng)式為

式中：的單位為弧度。

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

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

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

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

2.2 求根類

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

圖3 牛頓-瑞普遜法

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

將式（4）變形得到

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

當(dāng)?shù)恼`差在預(yù)先設(shè)定的可接受容限內(nèi)，則停止迭代，即

圖4 開平方根SCADE模型

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

表1 開平方根模型測試用例和測試結(jié)果

2.3 濾波算法類

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

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

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

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

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

進(jìn)一步得到對應(yīng)的差分方程

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

圖5 超前滯后校正模型的設(shè)計(jì)

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

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

圖7 超前滯后模型仿真結(jié)果對比

2.4 余度算法類

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

記輸入信號（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：若雙通道信號均有效，且信號偏差超過容許閾值，此時(shí)無法判斷哪個傳感器的信號有效，表決值為安全值（X_Safe），表決故障信息置為表決故障（VoteFault）；

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

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

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

使用SCADE真值表進(jìn)行模型設(shè)計(jì)，對應(yīng)的二余度表決SCADE模型如圖8所示。

圖8 二余度表決SCADE模型

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

圖9 使用SCADE進(jìn)行形式化驗(yàn)證的一般步驟

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

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

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

圖10 需求R1的驗(yàn)證模型

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

表2 R1形式化分析結(jié)果

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

3 結(jié)束語

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