在2013年前，Astrium是歐洲航空防務與航天公司(EADS: European Aeronautic Defence and Space Company)的一家子公司，主要提供航天民用和軍事系統及相關服務。Astrium在法國，德國，英國，西班牙和荷蘭都有分部。2012年的營收為58億歐元。

圖表1: 2013年之前EADS集團和其主要子公司

2013年末，鑒于AIRBUS的品牌知名度極高，EADS集團遂更名為AIRBUS Group。新組建的AIRBUS集團下轄3個業務部門：分別是負責民用飛機業務的Airbus，負責直升機業務的Airbus Helicopters和負責防務和航天業務的Airbus Defence & Space。其中的空客防務和航天分部是由Cassidian與Astrium合并組成。

圖表2: 2013年之后AIRBUS集團和其主要子公司

Astrium比較知名的業務有歐洲航天局(ESA: European Space Agency)主持的阿麗亞娜火箭(Ariane)的子系統、衛星、歐洲航天局(ESA)和美國國家航空航天局(NASA: National Aeronautics and Space Administration)聯合發起的火星探測車(ExoMars)、國際空間站的哥倫布號實驗艙和本篇要著重介紹的自動運載飛船(ATV: Automated Transfer Vehicle)。

圖表3: Astrium公司參與研制的部分產品

自動運載飛船原名阿麗亞娜運載飛船Ariane Transfer Vehicle，是歐洲航天局發起的用于國際空間站(ISS: International Space Station)貨物運輸的消耗性貨運航天器，具有較高的自主性，可自主與國際空間站交會對接。自動運載飛船由阿麗亞娜5號火箭發射到預定軌道，在2008年至2014年共成功運行了5次，五個自動運載飛船名稱分別是Jules Verne, Johannes Kepler, Edoardo Amaldi, Albert Einstein和Georges Lema?tre。自動運載飛船主要為國際空間站提供如下服務：

• 燃料補給

• 貨運交付，運輸包括推進劑、水、空氣、食物和科研設備等各種有效載荷

• 國際空間站的軌道修正

• 國際空間站的垃圾收集與銷毀

圖表4: Astrium的自動運載飛船ATV項目

自動運載飛船的安全關鍵模塊的軟件開發使用了SCADE，最初是使用版本V3。

圖為SCADE中定義的類型、常量、軟件架構和可激活塊。

圖表5: Astrium ATV項目中定義的SCADE類型、常量、軟件架構和可激活塊

SCADE定義的狀態機層級、子狀態機。

圖表6: Astrium ATV項目中定義的SCADE狀態機層級、子狀態機

建模完畢后，除了傳統的驗證活動外，Astrium公司還使用了法國國家科研中心(CNRS)以嵌入式系統研究著稱的VERIMAG實驗室的工具LESAR進行基于SCADE模型的形式化分析。LESAR工作原理同后期SCADE內嵌入的Prover工具一樣。(可參考 嵌入式系統 | 基于SCADE模型的形式化方法 一文)。最后將SCADE模型生成代碼，在項目中應用。

圖表7: Astrium ATV項目中基于SCADE模型和LESAR引擎的形式化方法工作流

2013年Astrium參與了歐洲啟動的旨在探索和研究安全關鍵領域如何簡化形式化方法應用的Hi-Lite項目。在該合作中Astrium重用了ATV項目中的SCADE模型，并結合基于Ada的SPAKR代碼的形式化分析方法，進行了技術驗證，獲取了一定的成果。下面對此進行簡要介紹。

Ada是20世紀70年代末美國國防部為了解決軟件危機而研制的通用程序設計語言，它是以Pascal語言為基礎開發實現的。Ada既繼承了眾多優秀高級語言的先進思想與技術，同時又融合了C++等流行語言的功能。Ada廣泛應用于安全關鍵領域的、長生命周期的大型軟件研發，在軍事、商業、公共交通、金融等領域的核心軟件開發中發揮著重要作用。迄今為止，國際標準組織先后確立過Ada 83,Ada 95,Ada 2005和Ada 2012共4個語言標準。取名Ada是為了紀念世界上第一位程序員Augusta Ada Lovelace女士。

20世紀70年代，C.A.R.Hoare提出了著名的Hoare邏輯并由此將斷言(Assertion)機制運用在程序設計語言中。斷言是指在適當的程序點添加預測語句并保證程序運行時刻預測語句一定成立。斷言機制的應用為保障程序正確性與提高程序可維護性提供了重要手段。例如，程序設計語言Euclid為構建可驗證的系統程序而設計，其既允許將斷言以注釋的形式交給驗證器進行處理，也允許將斷言寫成布爾表達式交由編譯器進行編譯，Euclid中的斷言成為驗證程序的重要手段。

隨著斷言機制在程序設計語言中的成功使用，基于斷言而產生的契約式設計思想于20世紀90年代被提出。與斷言相比，契約式設計的層次更高，概念也更加完善，可以看作一種軟件設計方法，這種方法要求軟件設計者為軟件組件定義形式化的、精確的、可驗證的接口，從而為傳統的抽象數據類型又增加了前置條件、后置條件和不變式。

契約式編程是契約式設計在程序設計語言上的應用，不僅為程序正確性和可維護性提供了保障，同時也是減少大型軟件開發成本的有效手段。

SPARK語言是一種基于Ada語言的形式化的計算機編程語言，適用于開發可預測的高可靠性的安全關鍵軟件。20世紀90年代，Praxis公司主持設計了第一個正式將契約機制與Ada程序設計語言進行組合而產生的SPARK程序設計語言。如今，SPARK被應用在空中管制系統等高安全性要求的領域。

針對Ada 83，Ada 95和Ada 2005分別對應SPARK 83，SPARK 95和SPARK 2005三個版本。SPARK語言的第四版是基于Ada 2012的SPARK 2014，該版本對語言和支持的驗證工具進行了重新設計。SPARK由一種編程語言，一個驗證工具集和一種設計方法共同構成，可確保將超低缺陷軟件部署在必須確保高可靠性的安全關鍵應用程序中。

圖表8: SPARK語言的構成

鑒于SPARK語言的成功實踐，WG9委員會的專家經過多番討論最終決定在Ada 2012中正式加入契約機制。Ada 2012中的契約由前置條件、后置條件、類型不變式和子類型謂詞等概念組成，可用于類型檢查、類型預測以及子程序維護等方面。另外，Ada 2012還允許在程序編程加入斷言對程序的執行狀態進行動態檢測。

SPARK 2014對契約使用相同的語法，這意味著用SPARK 2014驗證工具可以驗證用Ada 2012編寫的程序，而不必重寫契約。SPARK和完整Ada的子程序現在可以更輕松地共存。

圖表9: SPARK語言和Ada語言的主要差別

相比老版本Ada，SPARK 2014版本增加了自己aspect以進一步幫助靜態分析，這是對未經編譯或執行的源代碼進行的驗證。驗證使用執行靜態分析的工具。這些工具可以采取各種形式，包括類型檢查和執行可見性規則的工具(例如編譯器)，以及執行更復雜的推理(例如抽象解釋)的工具，如AdaCore的CodePeer之類的工具 。SPARK附帶的工具執行兩種不同形式的靜態分析：

• Flow analysis是最快的分析形式。它檢查變量的初始化，并查看子程序的輸入和輸出之間的數據依賴性。它還可以找到未使用的賦值和未修改的變量。

• proof檢查是否存在運行時錯誤以及程序是否符合其規范。

GNAT是Ada編程語言的免費軟件編譯器，它屬于GNU編譯器集合(GCC)的一部分。它支持Ada語言的所有版本，即Ada 83,Ada 95,Ada 2005和Ada 2012。GNAT項目始于1992年，當時的美國空軍授予了紐約大學(NYU)一份合同，為Ada構建免費的編譯器，以幫助Ada 9X標準化。GNAT的開發團隊后來成立了兩家公司，但始終是一個實體，2012年統一為AdaCore公司。

形式化驗證SPARK語言的工具稱為 GNATprove。它檢查與SPARK子集的一致性，并執行源代碼的flow analysis和proof檢查。其他幾種工具也支持SPARK語言，包括GNAT編譯器和GPS集成開發環境。GNATprove是后面將要介紹的Hi-Lite項目的一部分，是Ada的一個形式化驗證工具，它基于GNAT編譯器、Why3平臺和Alt Ergo prover。它可以證明子程序符合它們的契約。GNATprove目前可用于x86 linux、x86 windows和x86-64 linu

Ada程序通常包含兩個文件：

• 擴展名為ads的規范文件，包含契約，契約是用aspect編寫，體現了子程序的若干屬性

• 擴展名為adb的實現文件

僅以一個簡單案例說明使用SPARK aspects來驗證Ada子程序的契約。該子程序名稱為Increment，作用是將參數x加1。

• SPARK的Global aspect要求Increment子程序不讀寫任何全局變量

• SAPRK的Depend aspect要求參數x的調用僅依賴于調用前的x

• Ada的Pre和Post兩個aspect定義了Increment子程序的功能屬性

1. Pre aspect: 僅當x值小于Integer’Last時，Increment才可被調用。這確保子程序主體中的加法操作不會溢出。
2. Post aspect: x真的進行加法操作后，確保x比運算前的值大1

圖表10: Ada/SPARK程序中擴展名為ads的規范文件和擴展名為adb的實現文件

GNATprove可驗證這些契約。此外，它還可驗證執行Increment子程序時不會引起運行時錯誤。

圖表11: GNATprove對Ada/SPARK程序的形式化證明結果

SCADE R18及其以后版本的代碼生成器KCG 6.6支持將模型生成與SPARK 95版本兼容的Ada代碼。Suite KCG 6.6版本的Ada代碼生成器可通過DO-178C/DO-330 TQL-1等安全關鍵領域的工具鑒定。

Hi-Lite項目中開發工具由參與的所有合作伙伴(學術，工具開發者和最終用戶)自行指定，目的是驗證在真實項目中驗證形式化工具的實施情況。項目內容可以在下面列出的網址上查閱。

Hi-Lite項目定義了三個典型案例來進行研究，分別代表了不同的應用領域

• 航天領域：Hi-Lite工具在Astrium案例研究中的應用

• 功能安全與信息安全領域：Hi-Lite工具在各種不同SPARK示例和Tokeneer上的應用

• 終端用戶領域(Thales)：在面向組件的關鍵中間件的應用和工具集成

對于每個研究的案例又都分為兩個部分，1.描述案例的主要特征，2.總結使用Hi-Lite方法的益處。本篇著重介紹航天領域的案例，即由Astrium Space Transportation參與的研究，其結論是：在航天軟件甚至更普遍的安全關鍵實時嵌入式軟件中，形式化方法中是適用的。

根據歐洲航天領域的適用標準(歐洲空間合作組織標準化ECSS: European Cooperation for Space Standardization)，安全關鍵的實時嵌入式軟件的開發人員應該對詳細設計軟件和對應的測試程序進行歸檔。Hi-Lite項目的目標是1.研究對“詳細設計”進行形式化表述的方法和2.改進“形式化單元測試(Unitary Test)”的工具。

最初，由Astrium Space Transportation開發的每個軟件子程序(subprogram)是以非形式化方式的文本進行描述的，然后通過契約進行形式化表述為：

• 在何種條件下子程序可以被調用(前置條件)

• 子程序的預期行為(后置條件)，為了后續步驟(測試用例的描述)的方便，后置條件應盡可能地分解

為了沿用典型的測試流程，子程序的測試用例以非形式化地描述。測試用例的定義應該與詳細設計時測試用例的定義兼容。

• 測試用例在SPARK 2014中形式化

• 詳細設計和測試用例(兩者都以SPARK 2014格式進行形式化)的評審應該作為詳細設計評審(DDR: Detailed Design Review)和測試就緒評審(TRR: Test Readiness Review )的一部分

• 每個測試用例或者被形式化證明，或者被測試

• 測試規程被定義

應該確保覆蓋率：

• 軟件需求和詳細設計的覆蓋

• 詳細設計與測試規程的覆蓋

 典型的太空飛行程序大致由4個部分組成：

• 底層軟件，操作系統，驅動程序。這些軟件不在Hi-Lite考察范圍內

• 數據管理，此類軟件的典型應用是遙測和遙控，因為主要涉及對數據進行編碼和解碼，經分析也不太適合Hi-Lite研究

• 飛行控制或更一般的數值控制/指令算法

• 任務和飛船管理

Astrium的Hi-Lite項目主要涉及后面兩項。由于僅第三部分的飛行控制或更一般的數值控制/指令算法用到了SCADE模型，下面幾節主要對此作介紹。

數控/指令算法案例將浮點值作為輸入，執行一些數值計算(使用經典的基本數學運算符，例如加法，減法，乘法，除法，絕對值，三角函數或對向量和數組的運算等)并返回浮點型結果。這樣算法通常具有諸如內部狀態等上下文環境。

一般來說，定義精確的功能規約這些技術對這類代碼毫無用武之地。例如方程的功能規約X := A * Y + Cos(Z)就是表達式本身，幾乎不可能以更抽象的方法定義該公式。舍去精化公式的工作后，研究目的就是證明這類公式沒有運行時錯誤(例如除0)和確保范圍的正確性(例如，速度應該始終在0~25km/s之間)。

其中的太陽能帆板管理軟件(可用于ATV)就是以數值控制/指令算法為基礎實現的。該軟件負責

• 部署太陽能帆板(通過控制硬件鏈接來收放)

• 調整太陽能帆板的方位來優化接收的太陽能

太陽能帆板部署功能是用SCADE建模的，并用認證級的SCADE KCG Ada工具自動生成與SPARK兼容的代碼。SCADE建模、驗證、代碼生成等階段工作完畢后，接下來就需要評估Hi-Lite工具集分析自動生成代碼的能力。從SCADE模型生成的代碼示例如下:

圖表12: Astrium Hi-Lite項目中SCADE模型生成的

太陽能帆板的方位控制功能是手工編碼的，也需要評估Hi-Lite工具集分析算法手工代碼的能力。該部分代碼使用了數學庫，不過數學庫并非全部由SPARK 2014實現，即該部分不能形式化證明，只能進行常規測試。幸好數學庫的接口是符合SPARK 2014的，因此可用形式化方法證明上層的應用程序代碼。

數學庫契約的示例如下：

圖表13: Astrium Hi-Lite項目中某上層應用程序的SPARK手工代碼

應用程序代碼中定義的契約僅與變量范圍有關，示例如下：

圖表14: Astrium Hi-Lite項目中與變量范圍相關的契約SPARK手工代碼

所有契約均通過了動態測試檢查。然后是使用gnatprove進行形式化證明。如前述，證明兩部分

• Mathematical_Library

• Numerical_Algorithms

分析用時為233秒(3分53秒)。下表為子程序數量，分為3種：由SPARK 2014設計，非SPARK 2014設計和部分由SPARK 2014設計

圖表15: Astrium Hi-Lite項目中Mathematical_Library的分析結果

下表為驗證條件VC(Verification Condition)的分析，列的主要內容為

• VC被證明的數量

• VC未被證明的數量

• 百分比(VC證明和未被證明的)

• 總數

圖表16: Astrium Hi-Lite項目中Mathematical_Library的驗證條件的分析結果

關于未被證明的VC的原因分析：某些函數算法是GNATprove不能完全理解的。例如

圖表17: Astrium Hi-Lite項目中Mathematical_Library的無法證明的驗證條件

本例所示的Post契約無法通過GNATprove來證明。算法函數的精確行為取決于具體實現，這是可接受的。不能證明部分的解決方法是通過密集測試等傳統方法來驗證。

分析用時為653秒(10分53秒)。下表為子程序數量，分為3種，由SPARK 2014設計，非SPARK 2014設計和部分由SPARK 2014設計

圖表18: Astrium Hi-Lite項目中Numerical_Library的分析結果

下表為驗證條件VC(Verification Condition)的分析，列的主要內容為

• VC被證明的數量

• VC未被證明的數量

• 百分比(VC證明和未被證明的)

• 總數

圖表19: Astrium Hi-Lite項目中Numerical_Library的驗證條件的分析結果

關于未被證明的VC的原因分析有兩類。

Astrium希望評估的目標是，SPARK 2014應該滿足以下需求，

• 可以將測試用例形式化表述的能力

• 測試規程覆蓋測試用例的驗證(注: 測試用例，測試規程，測試結果)

• 支持驗證和確認沒有運行時錯誤

• 支持驗證和確認功能屬性

• 驗證訪問所有全局變量的正確性

• 驗證沒有超出范圍的值

• 軟件數據單位的內部一致性

  Hi-Lite工具應有助于確保每個集合都滿足軟件項目的要求。換言之，對子程序(subprogram)的每個調用都應確保符合被調用對象的前置條件，并且與被調用對象的后置條件兼容

• 評估可控性(commandability)和可觀察性(observability)的能力

  換言之，Hi-Lite工具應有幫助檢測死代碼的能力

• 幫助證明數值型數據的保護機制已正確實施

• 在特定情況下證明通用代碼的正確性

經過本案例分析后的，上述需求的評估結果為：

圖表22: Astrium Hi-Lite項目需求的評估結果

本篇介紹了航天領域Astrium公司將SCADE建模與SPARK編碼結合應用的經驗。

這種方法能結合兩種技術的優點，可以使工程技術人員早期在較高的層級上進行建模設計，而不是過早地拘泥于枯燥的編碼。當模型自動生成SPARK代碼后，又可以充分利用SPARK語法的特性和衍生工具，基于測試用例定義對應的含契約的規范代碼，并結合GNATprove等引擎進行更底層的編碼級形式化分析。

值得一提的是，唯有滿足以下兩點才能高置信度地融合兩種技術的優點：

• 選用模型背后的語言與SPARK代碼一樣，具有形式化的強語義。這樣既精確地描述業務邏輯，又能推遲繁瑣的代碼級驗證。

• 模型到代碼的過程是高可靠的，能確保精心設計的模型在生成代碼時不丟失其信息。

而SCADE恰好能符合這兩點。模型背后的Lustre語言是形式化，而可通過DO-178C/DO-330 TQL-1級工具鑒定的SCADE KCG Ada代碼生成器能確保模型和生成代碼是一一對應的。

選用這樣設計組合的好處是顯而易見的，可以獲得從模型到代碼的、一以貫之的、全面的、無縫銜接的形式化保證。而這又恰好體現了航天領域的參與者盡可能地提升產品安全性的不懈追求，以應對日益復雜多變的安全關鍵軟件的巨大風險。

[1] Olivier BOUDILLET. SCADE for a planetary lander demonstrator Astrium Space Transportation[EB/OL].SCADE User Group Conference 2013（內部文檔）

[2] David Lesens.SCADE Suite in Space Applications at EADS Astrium Space Transportation[EB/OL].SCADE User Group Conference 2008（內部文檔）

[3] 吳迪, 徐寶文. Ada 語言的發展[J]. 計算機科學, 2014, 41(1): 1-15, 38.

[4] Claire Dross and Yannick Moy.Introduction to SPARK[EB/OL]. https://learn.adacore.com/pdf_books/courses/intro-to-spark.pdf

[5] Hi-Lite partners. L7.2.2 Deliverable - Final report on experimentations on industrial case studies[EB/OL]. http://www.open-do.org/wp-content/uploads/2013/05/Industrial_Case_Studies_Final_Report.pdf

[6] Amey P, Dion B. Combining model-driven design with diverse formal verification[C]. 2006