近期推出的嵌入式系統(tǒng)專題內(nèi)容中，我們詳細梳理了Ansys SCADE的誕生、發(fā)展及應用，也針對“形式化方法”做了進一步闡述，詳實地介紹了在當今軟件行業(yè)已有眾多測試手段下為什么形式化方法尤為重要？本期我們將分享Ansys SCADE在航空電傳飛控系統(tǒng)中的應用。全文將從民用飛機的飛行控制系統(tǒng)、空客的電傳飛控系統(tǒng)、SCADE在空客電傳飛控中的應用、空客在研發(fā)選用的工具鏈中對形式化方法的重視以及案例展現(xiàn)等多個方面來闡述基于SCADE的形式化方法在空客電傳飛控中的具體應用。在后續(xù)專題內(nèi)容中我們還將推出包括軌道交通、核能重工及航天防衛(wèi)等行業(yè)應用案例。

飛機的飛行控制系統(tǒng)(FCS: Flight Control System)就是利用控制原理使得飛機的操縱面(又稱舵面,surface or rudder)偏轉(zhuǎn)，以實現(xiàn)對飛機的姿態(tài)和航跡運動進行穩(wěn)定控制的系統(tǒng)。飛控系統(tǒng)通常包括

• 飛行器運動，包括其重心的線運動、繞機體軸的角運動(升降舵Elevator完成俯仰Pitch，副翼Aileron完成滾轉(zhuǎn)Roll，方向舵Rudder完成偏航Y(jié)aw)，以及飛行器結(jié)構(gòu)模態(tài)的變化;

• 完成對飛機姿態(tài)和航跡運動的穩(wěn)定和控制所需的所有硬件及軟件

圖表1：飛行控制示意圖

通常認為，迄今為止飛控系統(tǒng)共演進了四代，分別是簡單機械控制系統(tǒng)、液壓助力控制系統(tǒng)、增穩(wěn)控制系統(tǒng)和電傳控制系統(tǒng)。采用電傳控制技術(shù)的飛機有幾大優(yōu)勢：

1. 相比傳統(tǒng)的機械控制系統(tǒng)的飛機有著更輕的重量，這是因為電傳飛控省去了機械傳動控制系統(tǒng)中的大量復雜、冗余的機械設(shè)備，減輕了系統(tǒng)部件的總重量，解放了飛機的內(nèi)部空間；

2. 電傳飛控的引入意味著飛機可以采用打破傳統(tǒng)氣動布局的靜不穩(wěn)定設(shè)計，使得飛機結(jié)構(gòu)內(nèi)部那些起著控制飛行穩(wěn)定性的部分零件省去或者減小比重，例如減小機尾的水平穩(wěn)定面與垂直穩(wěn)定面，減負后的飛機在航程與載重上都會有所提高，這對于特別考慮經(jīng)濟成本的民航而言有著重要的意義;

3. 使用了新一代飛控技術(shù)的民航客機極大增加了飛機的安全性，電傳技術(shù)的引入使得飛行員可以實現(xiàn)對飛機飛行姿態(tài)的微調(diào)，簡化操縱流程，提高駕駛精度，有效地預防飛行員過載、飛機失速等隱患。

電傳飛控系統(tǒng)分為模擬式和數(shù)字式兩種。前者使用模擬信號，后者使用數(shù)字信號，使用數(shù)字信號可以實現(xiàn)更多的狀態(tài)，使得飛行控制變得更加精細。而模擬式則只能根據(jù)相位，頻率，幅度的不同組合給出有限的幾個狀態(tài)來。

英國BAE和法國Aérospatiale 聯(lián)合設(shè)計的協(xié)和(Concorde)超音速客機是第一代應用電傳飛控技術(shù)的飛機，不過該飛控系統(tǒng)是模擬式的。第一代數(shù)字式電傳飛控系統(tǒng)出現(xiàn)在1980年初的空客A310上，該系統(tǒng)主要控制了縫翼、襟翼和擾流板幾個操縱面。1988年通過適航認證投入使用的A320使用了第二代電傳飛控技術(shù)，它可將高級控制律應用到所有的操縱面。

空客A320是世界上首個采用電傳飛控與靜不穩(wěn)定設(shè)計的民航客機。除此之外，A320還是業(yè)界首創(chuàng)使用側(cè)桿駕駛的民航客機。相對于傳統(tǒng)的中央操作盤，電傳側(cè)桿具有獨特的優(yōu)勢。首先，電傳側(cè)桿控制系統(tǒng)結(jié)構(gòu)精簡，重量輕，易于裝配和拆卸，維護成本明顯降低。其次，電傳側(cè)桿占用的駕駛艙空間較小，飛行員更易于觀察前方顯示器，為進一步優(yōu)化駕駛艙顯示、控制布局提供可能。最后，在臂托的配合下，駕駛員前臂相對固定，可以保證駕駛員操縱的穩(wěn)定性，減少駕駛員的工作負荷，降低操作難度。不管是中央操作盤還是側(cè)桿，都是通過推拉控制俯仰，通過左右轉(zhuǎn)動控制滾轉(zhuǎn)，通過腳蹬控制方向舵，即偏航。

圖表2：左側(cè)座艙的中央操作盤和右側(cè)座艙的側(cè)桿

空客設(shè)計的電傳飛控系統(tǒng)極其復雜，毫不夸張地說，這可能需要一整本書才有可能完整準確地描述，本文僅擇其要點進行簡單介紹。

為了滿足適航認證的要求，空客使用了9大“黃金法則”來研制其電傳飛控系統(tǒng)。

2.1.1 進行系統(tǒng)安全評估(SSA: Safety System Assessment)：評估每個功能失效對系統(tǒng)的影響。SSA使用故障樹方法，研究所有可能的失效組合，以確定事件發(fā)生的概率。每個基本失效的概率由相關(guān)設(shè)備的制造商給出，并根據(jù)經(jīng)驗重新評估或確認。

2.1.2 遵循嚴格的開發(fā)流程：主要基于ARP 4754/ED79(1996)系統(tǒng)開發(fā)標準，DO178B/ED12(1992)軟件開發(fā)標準和DO254/ED80(2000)硬件開發(fā)標準。

2.1.3 硬件冗余的設(shè)計：例如使用多臺電傳飛控計算機，操縱面的作動器使用不同的電源。A320/340使用3套電源(液壓驅(qū)動)，A380使用4套電源(2套液壓驅(qū)動和2套電驅(qū)動)。發(fā)動機引擎支持驅(qū)動液壓回路給網(wǎng)路供電。作為備份，沖壓空氣渦輪(RAT: Ram Air Turbine)也支持驅(qū)動液壓回路給網(wǎng)路供電。

2.1.4 監(jiān)控的設(shè)計：所有的飛控系統(tǒng)部件都需要實時監(jiān)控，例如傳感器，作動器和探針等。計算機的所有輸入和輸出也都需要監(jiān)控。例如，主控計算機發(fā)送伺服指令，需要監(jiān)控信息被正確地發(fā)送和接收。

2.1.5 重構(gòu)(Reconfiguration)的考慮：可對功能失效進行自動管理，這對飛機的容錯設(shè)計非常關(guān)鍵。重構(gòu)分為兩個層面：

2.1.6 非相似的設(shè)計:所有空客飛機都至少有兩種類型的計算機：一臺主控和一臺備份。它們的硬件和軟件都不一樣，也不是由同一個團隊開發(fā)的。上述系統(tǒng)級的重構(gòu)使用了主控計算機和備份計算機的切換，備份計算機比主控計算機簡單。非相似的設(shè)計也涉及作動器。在A380上使用了多種類型作動器：傳統(tǒng)的液壓驅(qū)動作動器(hydraulic Actuator)，新一代電驅(qū)作動器(EHA: Electro-Hydrostatic Actuator)和電動備用液壓作動器(EBHA: Electrical Backup Hydraulic Actuators)。EBHA在正常時是傳統(tǒng)的液壓作動器，在發(fā)生失效時可切換為電驅(qū)動作動器。

2.1.7 安裝的隔離考慮：計算機必須物理安裝在飛機上的不同地方，以避免在任何損壞的情況下完全失效。例如，發(fā)動機轉(zhuǎn)子爆裂會切斷為計算機供電的電線。同樣的原因，液壓系統(tǒng)和電氣系統(tǒng)的線路也要安裝在不同的地方。

圖表5：A380上飛控計算機安全位置的物理隔離

2.1.8 飛行控制計算機體系架構(gòu)：空客設(shè)計了含有命令計算機和監(jiān)控計算機的基本單元。每臺計算機各有一個命令通道(COM)和一個監(jiān)控通道(MON)。每個通道都監(jiān)視另一個通道。COM通道提供分配給計算機的主要功能(飛行控制律計算和操縱面的伺服控制)。MON通道主要確保對飛行控制系統(tǒng)的所有部件(傳感器、執(zhí)行器、其他計算機、探針等)進行永久監(jiān)控，并通過向COM通道和其他計算機發(fā)送故障檢測信號來觸發(fā)重構(gòu)。兩個通道彼此相鄰以方便維護。一臺計算機的COM和MON通道或者同時處于活動態(tài)，或者同時待機，或者再次同時激活變?yōu)榛顒討B(tài)。

A320飛控系統(tǒng)使用兩種計算機：ELAC(升降舵與副翼計算機:Elevator and Aileron Computers)和SEC(擾流板和升降舵計算機: Spoiler and Elevator Computers)。由于每臺計算機都有一個命令通道和一個監(jiān)視通道。因此，有四個不同的通道對應的四個不同的軟件包。除了ELAC和SEC之外，還有兩臺計算機用于方向舵控制(飛行增強計算機FAC: Flight Augmentation Computers)。它們不是ELAC和SEC的冗余。

A320飛控系統(tǒng)共由7臺計算機組成，包括2臺ELAC，3臺SEC和2臺FAC。這其中的ELAC和SEC共計5臺計算機組成了A320電傳飛控的主飛控計算機，5臺主飛控計算機中的任一臺都可以控制A320的飛行。

后續(xù)的A340和A380型號也使用兩種計算機：PRIM(主控計算機:Primary computers)和SEC(輔助計算機:Secondary Computers)。盡管計算機與A320是不同的，但基本的安全原則是相似的。

2.1.9 魯棒性的考慮：例如，沒有假的監(jiān)控警報、抗電磁干擾(EMI: Electro Magnetic Interference)和在嚴重雷擊、總風冷損失等情況下繼續(xù)運行的能力。

以下圖表6所示的是包含硬件冗余、非相似和系統(tǒng)重構(gòu)的電傳飛控架構(gòu)綜合視圖。頂部是A340飛機的雙翼，每個機翼上包含了內(nèi)側(cè)(Inboard)和外側(cè)(Outboard)的副翼(Ailerons)和6個擾流板(Spoilers)。在中部是左右兩個升降舵(Elevator)和中間的可配平水平安定面(THS: Trimmable Horizontal Stabilizer)。底部是方向舵(Rudder)，該方向舵由增強電氣結(jié)構(gòu)的腳蹬觸感配平單元(PFTU: Pedal Feel Trim Unit)組成，也連接著基本的機械結(jié)構(gòu)的備份控制單元(BCM: Back-up Control Module)組成，其方向舵的綠色操縱面由PFTU連接P1和S1冗余操作。

像擾流板這樣的非關(guān)鍵操縱面只需一個作動器驅(qū)動，而關(guān)鍵的操縱面需要與兩個甚至三個作動器相連。每個作動器與某顏色表示的液壓回路相關(guān)聯(lián)(例如,Y表示黃色等)。P表示主控計算機，S表示輔助計算機。對于帶有冗余作動器的操縱面，箭頭顯示了重構(gòu)邏輯。例如，在左側(cè)升降舵上，P1是主控計算機，控制綠色作動器，P1和綠色作動器都處于主動態(tài)；P2是輔助計算機，控制藍色作動器，P2處于待機態(tài)，藍色作動器處于被動態(tài)。如果P1主控計算機、或綠色作動器、或綠色液壓回路出現(xiàn)故障，則自動重構(gòu)將P2設(shè)為主控計算機，藍色作動器設(shè)為主動態(tài)(同時綠色作動器設(shè)為被動態(tài))。如果當前主動態(tài)再失效，下一個重構(gòu)是P2到S1；再失效的重構(gòu)是到S1到S2，可見輔助計算機也可作為冗余備份。

圖表6：A340電傳飛控的操縱面架構(gòu)綜合視圖

飛行控制計算機的主要任務(wù)之一就是計算飛行的控制律。根據(jù)飛行員的指令(側(cè)桿或腳蹬)、飛機的運動傳感器和大氣數(shù)據(jù)傳感器信息來計算，其結(jié)果是操縱面按照指令偏轉(zhuǎn)，以實現(xiàn)所需的飛行軌跡修改。作動器會驅(qū)動操縱面偏轉(zhuǎn)到指定的位置。

在飛控計算機中，通常從3個冗余的大氣數(shù)據(jù)慣性基準單元(ADIRU: Air Data Inertial Reference Unit)中接收各自檢測到的大氣和慣性數(shù)據(jù)值，再為控制律計算所需的飛行參數(shù)。這種專門的處理，稱為“合并”(consolidation)或“三余度處理”(Triplex)，通常分為兩步：首先從3個獨立ADIRU源中表決得出準確的參數(shù)；其次監(jiān)視3個獨立源，舍棄任何失效的源，并確保選擇的數(shù)據(jù)是正確的。這種多數(shù)表決機制是較成熟的技術(shù)，在現(xiàn)代電傳飛控系統(tǒng)中使用廣泛。

圖表7：飛行控制律計算的通用原理

在大型民用飛機上，飛控計算機的計算能力比其他傳統(tǒng)的非關(guān)鍵應用(例如，多媒體)要低，這是因為安全關(guān)鍵的應用程序必須使用經(jīng)過驗證的，可靠的處理器。例如，A340主控計算機處理器是頻率為32 MHz的AMD 486 DX4，每秒大約處理1900萬條指令。由于處理器配置較一般，盡管計算的負擔相當繁重，但諸如非線性濾波“矩陣三角化”，“在線優(yōu)化算法”，“傅里葉變換”或“小波計算”等高級處理算法依然較難使用。所以必須刪除所有不必要的計算和冗余數(shù)據(jù)，以盡可能精簡開發(fā)出來的復雜算法。然而這種算法的簡化又會出現(xiàn)性能的損失，這就需要設(shè)計者們找到復雜度和高性能之間的折衷平衡。

由于典型的空客飛控計算機包括兩個獨立的通道，每個通道都有自己的時鐘。因此，兩個單元之間存在時間異步。而飛控計算機是多速率時間觸發(fā)的，這意味著即使在同一個單元中，所有的數(shù)據(jù)也不是在同一采樣周期內(nèi)處理的。例如，某些數(shù)據(jù)每40 毫秒采樣生成，而算法邏輯的計算周期是每10毫秒，這就需要使用預測濾波器等方法修改算法邏輯使其適配采樣時間。這是電傳飛控的設(shè)計需要認真考慮的因素。

圖表8: A340和A380飛控計算機配置的對比

從1980年代開始，A320系列客機的電傳飛控軟件開發(fā)中就使用了Aérospatiale推出的SAO (Computer-Assisted Specification)工具（詳見：嵌入式系統(tǒng) | 細數(shù)Ansys SCADE的前世今生）。電傳飛控的技術(shù)規(guī)范中準確地定義了需要由軟件實現(xiàn)的功能，主要內(nèi)容有：各傳感器信息獲取與監(jiān)控功能、飛行控制律功能、監(jiān)控功能、操縱面修正功能和重構(gòu)功能。

SAO可通過一組有限的圖形符號(加法、濾波、積分、查找表等)來描述預先定義在功能規(guī)范表(functional specification sheets)內(nèi)的每個部分。

圖表9：SAO工具開發(fā)A320的控制律

在后續(xù)的其他空客系列(例如: A340，A380和A400M等)研制中轉(zhuǎn)而使用更成熟的下一代工具SCADE(Safety Critical Application Development Environment)。

圖表10：SCADE工具開發(fā)A340、A380的控制律

使用這種基于形式化語言的模型開發(fā)工具，通常分為兩個步驟。第一，根據(jù)軟件技術(shù)規(guī)范進行建模。不同型號的飛機可以通過橋接的配置管理工具，方便快捷地復用相關(guān)的設(shè)計，并自動化地進行語法語義檢查。第二，通過認證的工具可以自動將設(shè)計完畢的模型生成可在飛控計算機中直接運行的代碼。

圖表11：飛控計算機的軟件實現(xiàn)概覽

使用SCADE工具進行開發(fā)是電傳飛控軟件容錯設(shè)計的重要手段，對安全性有積極作用。自動化的工具確保了即使需要快速實現(xiàn)對規(guī)范的修改(例如在飛行測試階段遇到的情況)，也能輕松勝任。完成后還可以很容易地實現(xiàn)自動代碼生成。支持在設(shè)計過程的早期進行“非回歸”測試，以檢查有效性及是否存在由于變更而導致的錯誤。這些測試應該盡可能早地執(zhí)行，以盡量減少開發(fā)階段的調(diào)試工作。

下方圖表12為伺服控制驅(qū)動某操縱面的功能規(guī)范圖示例（部分）。該規(guī)范只使用了非常基本的符號：加法、增益、門限、邏輯門和選擇開關(guān)。輸入是三角形符號的布爾類型條件和浮點型的真實信號(表示命令、位置等)。輸出是浮點型信號數(shù)據(jù)和對作動器的模擬硬件輸出(黑色輸出表示)。該邏輯描述了某操縱面的伺服器使用比例積分(PI: Proportion Integration)進行控制的通用方案。將請求的操縱面位置的命令值與作動器內(nèi)部專用傳感器實際測量的操作面位置值進行比較。由此產(chǎn)生的控制回路誤差乘以適當?shù)脑鲆?K1或K2)以輸出到底下第一個輸出值current。為了補償作動器級的任何可能的偏差，在第一個輸出值中添加適當?shù)难a償Bias值(PI控制的積分部分)，以提供發(fā)送到執(zhí)行器的第二個輸出值current_c。該偏差Bias的計算在另一張功能規(guī)范圖中定義，并未在當前圖中標識。伺服閥接收計算后的總輸值出current_ano，并將其轉(zhuǎn)換為作動器內(nèi)的液壓流體運動，最終控制與操縱面相連的作動器桿移動到相應位置。

圖表12：伺服控制某操縱面的功能規(guī)范圖案例

功能規(guī)范圖還包含諸如飛機類型、計算機類型、特定功能、采樣周期、版本(修改次數(shù))、設(shè)計者姓名等信息定義。據(jù)統(tǒng)計，A380的主控計算機大約有5000個專用的功能規(guī)范圖，A380的輔助計算機大約有3000個專用的功能規(guī)范圖，可見相關(guān)計算的工作量是極其巨大的。設(shè)計中還需要將功能規(guī)范圖進行級聯(lián)排序，以便一張接一張的計算，以最小化信號間的延遲，再由SCADE工具進行實現(xiàn)。

圖表13：SCADE實現(xiàn)A380飛控輔助計算機的某功能規(guī)范圖

而空客在開發(fā)過程所用的形式化工具及其在各階段的對應關(guān)系如何，本節(jié)將針對空客電傳飛控產(chǎn)品的研發(fā)流程中使用的形式化方法工具鏈進行介紹。

圖表14:空客開發(fā)流程

空客將形式化方法應用到以下產(chǎn)品的軟件開發(fā)驗證流程中。

圖表15：空客應用形式化方法開發(fā)的產(chǎn)品

從上期《基于SCADE模型的形式化方法介紹》一文中我們知道，形式化方法分為三種，抽象解釋、模型檢查和演繹法。在空客研發(fā)的包括電傳飛控系統(tǒng)等安全關(guān)鍵軟件中用過如下的形式化方法工具。

圖表16：空客使用的形式化方法相關(guān)的工具

Frama-C意思是“C代碼的模塊化分析框架”，是A framework for modular analysis of Ccode中藍色字的縮寫。它是由CEA和INRIA研發(fā)的開源軟件，可基于不同理論對C源代碼進行靜態(tài)分析。靜態(tài)分析是從源代碼中提取一定數(shù)量的信息，而不運行它。Frama-C允許以抽象解釋等方法對給定程序檢查是否存在可能的運行時錯誤，例如，對初始化指針的引用、溢出、除零等。

Frama-C中實現(xiàn)信息提取的技術(shù)主要有抽象解釋和演繹方法。Frama-C基于核(kernel)，且使用同一種形式化規(guī)約語言ACSL即標準C規(guī)約語言(ANSI C Specification Language)對C源代碼做標注(annotation)，因此基于Frama-C開發(fā)的插件可使不同的靜態(tài)分析在同一標注代碼上進行協(xié)作。

圖表17：Frama-C架構(gòu)和插件

這些插件利用了Frama-C平臺提供的幾個內(nèi)核和基本服務(wù)來計算用戶需要的結(jié)果。這些結(jié)果包括抽象語法樹、證據(jù)項目管理、命令日志、每個函數(shù)甚至C表達式的I/O計算、程序依賴關(guān)系圖、控制流、數(shù)據(jù)流、代碼切片、影響分析、死代碼或無法訪問的代碼的檢測等。

圖表18：Frama-C常用插件介紹

盡管在數(shù)學中，實數(shù)的精度是無限的。但在工程實踐中，實數(shù)的精度有限的，通常為單精度浮點數(shù)(float)和雙精度浮點數(shù)(double)。因此，在進行浮點運算時，四舍五入等錯誤會影響結(jié)果。另外，在理論演算時穩(wěn)定的計算在工程實踐中也可能不穩(wěn)定。CEA公司開發(fā)了Fluctuat，可用于分析C源代碼程序在特定處理器上數(shù)值精度。可以：

• 確保浮點數(shù)表示的變量精度在程序全周期有效

• 如果運算涉及浮點數(shù)，確保浮點數(shù)與實際浮點數(shù)的誤差在程序全生命周期內(nèi)的精度可控

除此之外，F(xiàn)luctuat還可以協(xié)助用戶找到代碼中浮點數(shù)的問題。諸如缺乏精度、不穩(wěn)定、靈敏度等。空客的電傳飛控系統(tǒng)中不少基礎(chǔ)庫是用SCADE實現(xiàn)的，用Fluctuat進行檢查后獲得了較好的結(jié)果。

Astree是基于抽象解釋的靜態(tài)分析器，能夠證明用C語言編寫的程序中沒有運行時錯誤。它最初由Ecole normale supérieure的計算機科學實驗室開發(fā)，現(xiàn)在屬于AbsInt公司。因為是基于抽象解釋理論，所以它可能會產(chǎn)生虛假警報。為了使其能安全關(guān)鍵領(lǐng)域的工程上得到應用，對其做了改進。改進后的Astree對基于同步語言的控制設(shè)計軟件SCADE（或SAO，SCADE前身）尤其適用，其分析結(jié)果的精度極高（虛假警告幾乎為零）。其可擴展性、適用性為也極佳，在可接受的時間內(nèi)成功分析了50萬行代碼。

aiT是AbsInt公司的一套工具，可用于計算飛機、汽車等不同微處理器的最壞運行時間(WCET: Worst-case Execution Time)。這些工具有一個可執(zhí)行程序和一個標注文件(給工具的指令)作為輸入。標注中，目標板外部存儲器和總線的描述是以含有相關(guān)訪問時間的地址區(qū)域列表形式出現(xiàn)的。計算WCET前還需要用戶提供任務(wù)的起始點。被分析的程序必須是順序執(zhí)行的(沒有多線程，并行或等待外部事件)。

該工具首先構(gòu)建程序的控制流圖(CFG: Control Flow Graph)。接下來分別進行值分析(value analysis),緩存分析(cache analysis)，管道分析(pipeline analysis)和路徑分析(path analysis)。

值分析計算寄存器和地址在內(nèi)存訪問時的值間隔，其中的循環(huán)界限分析階段要確定可能的循環(huán)迭代次數(shù)上限，由正在分析的任務(wù)來預測地址的計算，并排除后面分析中不可能的路徑。

緩存分析使用值分析的結(jié)果預測緩存的行為。它將對內(nèi)存的訪問分類為“命中”、“未命中”或“不確定”。緩存分析可以在緩存未命中的情況下預測下面管道停止的情況，特別是在命中或未命中分類的情況下，可減少了不確定情況的數(shù)量。

管道分析是相當于在目標處理器模型上的程序執(zhí)行，該程序是由安全符號組成的CFG。管道分析利用前面分析的結(jié)果，預測所分析任務(wù)的時間行為，并計算所有基本塊的WCET，基本塊是指由跳轉(zhuǎn)或程序調(diào)用完成的匯編程序指令序列。

路徑分析計算任務(wù)最長的執(zhí)行路徑。路徑分析使用整數(shù)線性規(guī)劃(integer linear programming)技術(shù)，求其上界得出結(jié)果。

WCET將程序分離為若干個斷續(xù)的階段使得每個階段的技術(shù)應用成為可能。對值、緩存和管道的分析是用靜態(tài)分析和抽象解釋技術(shù)。當前Ansys公司SCADE Suite產(chǎn)品中含有該模塊。

圖表19：PowerPC MPC755 aiT/WECT

Stackanalyzer是AbsInt公司的工具。以二進制形式分析程序堆棧的使用，計算實際內(nèi)存使用量的上限。該靜態(tài)分析有助于證明沒有程序執(zhí)行引起的堆棧溢出。當前Ansys公司SCADE Suite產(chǎn)品中含有該模塊。

Lesar是使用二元決策圖(BDD: Binary Decision Diagram)對基于Lustre語言模型進行模型檢查的工具，其算法用于枚舉可達狀態(tài)。

L4是Prover Technology公司開發(fā)的可對SCADE模型進行形式化驗證的插件，可提供類似Lucifer的功能，但界面更加友好，可以與SCADE集成開發(fā)環(huán)境無縫連接。

-Tools是Prover Technology公司基于St?lmarck證據(jù)流程的的通用驗證工具。

L4、-Tools和Lucifer都是Prover Technology公司提供的針對SCADE模型進行形式化驗證的早期版本。只能處理整型數(shù)據(jù)類型。

SCADE Designer Verifier是當前Ansys公司SCADE Suite產(chǎn)品的標準形式化驗證模塊。

由CEA開發(fā)的C代碼靜態(tài)分析工具，可用于驗證安全關(guān)鍵軟件。主要基于霍爾邏輯(Hoare Logic)和一階邏輯謂詞(first order logic predicates)進行最弱前置條件的計算。Caveat集成了3款工具:代數(shù)式簡化器(algebraic simplificator)，自動定理證明器(demonstrator/automatic theorem prover)和交互式預測轉(zhuǎn)換器(IPT: interactive predicate transformer)。Caveat是空客在90年代為C代碼程序使用的形式化驗證工具，2006年后轉(zhuǎn)而使用后繼產(chǎn)品Frama-C。使用Caveat的形式化方法符合《DO-333》中介紹的Unit Proof方法，主要是針對手寫C代碼的，其對應的形式化的低層需求(LLR: Low level Requirement)是由一階謂詞邏輯設(shè)計。

新版DO-178C系列中A-7表第9個目標是：驗證無法追蹤到源代碼的附加代碼。該目標是DO-178C標準新加的，將原標準中的隱性目標明確化了。航空軟件的驗證通常會在源代碼級執(zhí)行結(jié)構(gòu)覆蓋，然而由于可執(zhí)行目標碼是實際飛行的代碼，所以對于A級軟件，需要有一些分析來確保編譯器沒有生成不可追蹤的或不確定的代碼。但是，編譯器是非常復雜的軟件，特別是對于C語言這類全功能通用語言的處理更為復雜，直接對編譯器進行驗證極為困難。因此，業(yè)內(nèi)并不存在通過了工具鑒定的通用C語言編譯器。

為了解決該問題，2008年12月開始空客和INRIA合作開展了CompCert編譯器項目，該編譯器最初由INRIA計算機專家Xavier Leroy領(lǐng)銜研發(fā)，是經(jīng)過形式化驗證的可信編譯器的杰出代表。該編譯器將C的一個重要子集Clight翻譯為PowerPC匯編代碼(后來也支持IA32和ARM后端，目前已擴展至可支持64位處理器)，其編譯過程使用了11中語言，并劃分為多個階段，每個階段的翻譯正確性都借助工具Coq進行了證明，且這些證明可由獨立的證明檢查器檢查，這是迄今最強的形式化驗證手段，達到了人們所能期望的最高可信程度。CompCert對目標碼也做了包括簡化控制流和數(shù)據(jù)資源智能使用的優(yōu)化，其最壞運行時間提升12%左右。

圖表20：CompCert開發(fā)工作流

下圖為空客的基于CompCert編譯器的工具鏈配置。

圖表21：空客基于CompCert編譯工具鏈

圖表21右上角的Airbus ACG是空客在SCADE KCG基礎(chǔ)上定制的自動代碼生成器工具(Automatic Code Generator)。其詳細內(nèi)容如圖表22所示，該定制工作保持Suite模型到C代碼前端不變，又在后端增加了可適配不同硬件平臺、不同處理器和編譯選項，不同框架代碼的處理。所有定制工作不影響SCADE模型和生成的代碼。前端后端合并后，可一起通過DO-178B的工具鑒定。

圖表22：空客基于SCADE KCG定制的自動代碼生成器

綜上，用一張圖來描述空客使用的各形式化分析工具在其開發(fā)流程中的對應關(guān)系

圖表23：空客的形式化分析工具在開發(fā)流程階段的對應關(guān)系

空客從A320開始使用了SCADE來開發(fā)模型，在A340、A380和A400M等型號開始對SCADE做了模型檢查等形式化分析。這些工作主要由空客和法國國家航空航天研究中心(ONERA)協(xié)作研究完成，使用的模型檢查引擎主要是Prover Technology公司提供的。

先簡述一下空客典型的模型檢查驗證框架。該框架包含3個部分：SCADE模型，待驗證的屬性(P: Property)和系統(tǒng)環(huán)境相關(guān)的假設(shè)(H: Hypothesis)。基于SCADE的模型檢查，就是驗證在給定假設(shè)的前提下，模型滿足預設(shè)的屬性。

假設(shè)H用于在整個分析過程中對輸入進行約束，它不是唯一的，也不是必須的。屬性P的識別和提取是難點，通常有兩種方法：和系統(tǒng)設(shè)計者討論得出，或者研究安全相關(guān)的設(shè)計文檔和驗證文檔。屬性提取后，以獨立的布爾型輸出變量表示出來。當SCADE模型滿足該屬性，則屬性P結(jié)果恒為真，即通過模型檢查。當屬性P結(jié)果為假，則模型至少存在一個錯誤，該錯誤可由模型檢查器返回的反例來重現(xiàn)。下面介紹幾個案例。

圖表24：空客基于SCADE的模型檢查證框架

如前所述，電傳飛控系統(tǒng)由主控計算機和輔助計算機組成。其中的計算機使用SCADE實現(xiàn)了功能規(guī)范圖，包括輸入驗證，邏輯處理，控制律，伺服控制等。設(shè)計師提出兩個安全需求屬性。

首先是關(guān)于側(cè)桿控制的功能。飛機有主駕副駕兩位飛行員，每個飛行員都有一個側(cè)桿可以操縱。

P1：兩個側(cè)桿不可同時發(fā)生故障，任意時刻必有一個側(cè)桿處于活動狀態(tài)。

第二個是關(guān)于內(nèi)副翼的功能。對副翼操縱面有主控計算機PC1，PC2，兩個輔助計算機SC1，SC2。

P2：如果兩個主控計算機PC1和PC2都發(fā)生故障，則輔助計算機SC1開始運行。

在精化這兩個屬性前，先簡要介紹下常用的一階謂詞邏輯，這在推理證明中是比較常用的

圖表25：常用的一階謂詞邏輯

P1屬性的不足之處在于當前“活動”側(cè)桿的定義方法。可以考慮根據(jù)側(cè)桿傳輸?shù)闹噶顏矶x當前“活動”的側(cè)桿。因為主駕副駕的指令可以傳送到操縱面。P1屬性改為

也就是說，如果主駕指令不等于0或副駕指令不等于0，則傳輸順序不等于0。然而，由于計數(shù)器等原因，該屬性表達式是錯誤的。確實存在一個側(cè)桿已經(jīng)發(fā)生故障，另一個側(cè)桿正在運行且值為0的情況。即處在“雖然屬性P1是false，但實際上是有效的”狀態(tài)。問題的關(guān)鍵是：活動的的側(cè)桿未發(fā)送指令，或活動的側(cè)桿發(fā)送了指令但指令為0。所以如果需要從傳輸指令的角度判斷，需要更深入規(guī)范，可以從另外一個角度來分析。P1的另外一種表達方式

該P1的含義是：不存在這樣的情況，即主駕有優(yōu)先權(quán)且主駕的側(cè)桿故障，或副駕有優(yōu)先權(quán)且副駕的側(cè)桿故障。本例說明非形式化文本轉(zhuǎn)換到形式化表達式是有個過程的，是不容易的。

屬性P1描述完畢后，應用模型檢查引擎(基于Lucifer和Lesar)就行分析。除了一個反例外，最終被證明是有效的。該反例是初始化時兩個側(cè)桿都失效了，所以再添加一個簡單的假設(shè)即可。

仔細看P2定義，其實不完整，還隱含兩個重要的功能。更精確地分析后，得出第一個隱含功能：

1. 當PC1和PC2都故障時，如果SC1可以用，則用SC1；

   如果SC1也不可用，則需要判斷SC2是否可用。表達式可以寫為：

   P2:   if (兩個主控計算機PC1和PC2 都發(fā)生故障)

   then if (輔助計算機S1是否可用)

   then (輔助計算機 SC1 運行)

   else (申請輔助計算機SC2 是否可用)

   else (輔助計算機 SC1不可用)

    

2. 第二個隱含功能推薦反向推導，如果PC1和PC2沒有同時發(fā)生故障，則SC1不可用。

   該語句可以表述如下：

   P2b:  if not (兩個主控計算機PC1和PC2 都發(fā)生故障)

   then not (輔助計算機SC1可用)

   再次反推簡化，如果SC1是可用的，則PC1和PC2必然都發(fā)生故障了。

   P2b:  if (輔助計算機SC1是可用的)

   then (兩個主控計算機PC1和PC2都發(fā)生故障)

輔助計算機SC1可通過檢查由它管理的兩個主控計算機門是否關(guān)閉了，來判斷其自身是否可運行。使用一階邏輯謂詞的表達式為

屬性P2b描述完畢后，應用模型檢查引擎(基于Lucifer)分析后，發(fā)覺除了在初始化階段系統(tǒng)不穩(wěn)定的情況外，其他時候都是有效的，所以添加了begin_ok操作符，使之屏蔽最初運行的幾個周期，只關(guān)注后續(xù)穩(wěn)態(tài)的行為。新增假設(shè)為：

本案例中的SCADE模型還包含了很多浮點數(shù)變量。但是早期的Lucifer對浮點數(shù)的支持能力一般，只能處理布爾和整數(shù)。方法是將浮點數(shù)轉(zhuǎn)換成整數(shù)，案例中采用了以下方法：首先找到所需的精度，然后將每個浮點數(shù)與之相乘，將其轉(zhuǎn)換為整數(shù)。本例中我們將浮點數(shù)乘以100。這種轉(zhuǎn)換會可能會給驗證帶來問題，但能得出有意義的結(jié)果，在前期就確保了不會出現(xiàn)重大問題。

考慮某基礎(chǔ)模塊“復位偏置鎖存器”操作符(the reset-biased latch operator)，含有Set, Reset兩個輸入，output一個輸出。該鎖存器的初始態(tài)output為false。只要輸入Set為true且輸入Reset為false，則output必為true。除此之外，output延遲的運行結(jié)果必為false。

圖表26：復位偏置鎖存器模型 reset-biased latch

現(xiàn)有某擾流板的氣閘(air brake)要調(diào)用該鎖存器操作符，設(shè)計氣閘控制模型airBrakeControl。

圖表27：原氣閘控制模型airBrakeControl(待形式化分析驗證來修正錯誤)

設(shè)計內(nèi)容如下：

設(shè)計師提出安全需求屬性為：不存在輸出airBrakeExtension和輸出airBrakeRetraction同時為true的情況。設(shè)計屬性表達式如下

屬性P為：Not (airBrakeExtension and airBrakeRetraction)

從物理上來說，輸入airBrakeLeverOn和輸入airBrakeLevelOff同時為true,相當于氣閘上的操縱桿同時設(shè)置為on和off，這是不可能的。因此可以設(shè)計

假設(shè)H為：Not (airBrakeLeverOn and airBrakeLevelOff)

將原模型，屬性P和假設(shè)H設(shè)計到同一張頁面后的總SCADE模型如下：

圖表28：氣閘控制模型的形式化分析頁面

應用SCADE Design Verifier引擎進行第一次分析，得出該airBrakeControl操作符不滿足屬性P，得到一個反例。該反例由兩個周期組成：

圖表29：修改后的氣閘控制模型airBrakeControl

對A340的500-600型號的電傳飛控輔助計算機的多個方面做形式化分析能力的驗證，結(jié)果如圖表30。主要對12個基于SCADE的模型進行評估，從三個方面驗證模型檢查的可用性。

1. 多處理器方面。空客的電傳飛控系統(tǒng)運行在異步容錯的多處理器架構(gòu)；

2. 多速率組方面。系統(tǒng)的不同代碼在不同速率組的運行；

3. 數(shù)值計算方面，例如二階濾波器，含有復雜的浮點數(shù)運算等。

共試驗了12個模型，從最右側(cè)那列可以看到結(jié)果。Yes代表可以進行形式化分析，F(xiàn)ailure代表不能。形式化分析結(jié)果無論是對或錯，都是Yes,即具有形式化分析的能力。分析的結(jié)果是沒有，就是Failure，即無形式化分析的能力。中間三列若都沒有勾選符號√，代表是單處理器且單個時鐘的架構(gòu)。

圖表30：形式化能力的驗證結(jié)果

顯而易見，3,8,9三項的模型是單處理器單時鐘架構(gòu)，天然可以做模型檢查。

考慮通信延時(communication delays)和時鐘異步(clocks asynchrony)設(shè)計，會加劇模型的復雜度。1,2,7三項是相對簡單的模型，因此也可以做模型檢查。由于早期SCADE不太擅長處理異步行為，所以10這項失敗。對復雜的設(shè)計需要權(quán)衡模型精確度和狀態(tài)空間爆炸。

對僅僅是多速率組的情況，也可以進行模型檢查，可以用專門的工具插入手寫代碼實現(xiàn)多速率組。第5項是含有100頁內(nèi)容的SCADE模型，且運行在4個不同速率組。

第11項是相對簡單的浮點數(shù)運算的模型檢查，也成功。

4,6,12三項是浮點數(shù)相關(guān)的非線性運算，現(xiàn)有的形式化分析引擎較難應對，不可進行形式化分析。

案例四是A380擾流板功能。擾流板展開后，可用于減少飛機升力，促進剎車效果。需要驗證：在飛行中，擾流板不可過度展開。該功能主要是布爾邏輯組成，僅有部分基礎(chǔ)的數(shù)值計算（門限比較，整數(shù)運算），有時間計時器。限于商業(yè)涉密的資料，公開信息不多，盡管詳盡的分析過程資料有限，但公開的分析報告結(jié)果也足以說明形式化分析的作用。

案例四有兩個版本的功能設(shè)計，一個是有錯誤的版本，一個是正確的版本。有錯誤的版本在常規(guī)測試未發(fā)現(xiàn)錯誤，在實驗室的飛行動力學測試后發(fā)現(xiàn)錯誤。盡管擾流板功能涉及的數(shù)值計算不多，但由于存在較多的計時器設(shè)計和布爾邏輯處理，因此依然足夠復雜。

在配置為256M內(nèi)存、1.7GHz的Pentium 4處理器上對“正確版本模型”進行形式化驗證，分析了48小時，得出正確的結(jié)論。而對“不正確版本的模型”進行的形式化分析，其反例的產(chǎn)生時長為幾分鐘到一小時，這取決于選用SCADE策略(見《基于SCADE模型的形式化方法》介紹)的檢測深度。反例運行的深度范圍是50~160之間。

通過以上對多個案例的分析，研究人員在空客電傳飛控的形式化方法應用上得出以下的經(jīng)驗與收獲。

關(guān)于屬性P的設(shè)計。縮小非形式化的安全需求與形式化的安全屬性的差距，需要花不少功夫。

關(guān)于假設(shè)H的設(shè)計。研究表明有兩類假設(shè)：1.排除不合理行為的假設(shè)，2.便于自動化分析而簡化驗證的假設(shè)。對于第一類假設(shè)，實際上并不容易區(qū)分該假設(shè)對應的行為是否真不合理，確定有效的輸入閾得由飛行動力學試驗來解決。第二類假設(shè)是故意排除了一些合理的行為，例如起落架輪分析時，會假設(shè)輪子靜止不動或保持勻速旋轉(zhuǎn)。假設(shè)縮小了驗證范圍，但該范圍較難排除所有不合理的行為。

關(guān)于反例的解釋。形式化分析證偽得出的反例需要進一步分析，可能是假設(shè)不足引起的不合理行為，也可能是對應真實飛行場景的反例。常規(guī)測試出現(xiàn)的錯誤，可以通過時間圖觀察可視化的航跡來定位模型的錯誤。形式化驗證的反例較難應用時間圖，因為有些反例從物理角度看來毫無意義。盡管有些不合理的細節(jié)，但反例可能恰恰揭示了模型中的真正問題。推薦用兩個方法縮小范圍來分析反例：1.識別反例隨時間變化的模型結(jié)構(gòu)部分；2.基于反例構(gòu)建一個有意義場景，再來觀察。第一個方法較容易，只要方案被精確定義。第二個方法較難，需要專業(yè)的航空領(lǐng)域知識。

圖表31：形式化分析的方法

迭代的過程。形式化分析不是按個按鈕的問題，需要探索分析迭代進行。產(chǎn)生反例可能是模型的缺陷，也可能是屬性P的問題，也可能是假設(shè)H的不足。

綜上，空客在電傳飛控系統(tǒng)上應用的形式化方法是有效的，模型檢查是切實可行的手段。盡管后期實驗室的飛行動力學測試和飛行測試也能找到飛控模型的缺陷，但這個階段再修改錯誤的代價就較高了。前期形式化分析階段就能暴露的問題體現(xiàn)了軟件行業(yè)“越早發(fā)現(xiàn)缺陷，成本越低”的金科玉律。