在正式采用新的DO-178C / ED-12C標(biāo)準及其補充（包括關(guān)于形式方法的DO-333 / ED-216補充）五年后，尚未有航空電子認證項目承認使用這一新補充。然而，確實存在形式化的方法技術(shù)，可以簡化航空電子軟件的開發(fā)。

阻礙采用正式程序驗證進行航空電子認證的主要障礙是，盡管開發(fā)DO-333 / ED-216的委員會進行了大量的傳播工作，但缺乏關(guān)于如何應(yīng)用DO-333 / ED-216的普遍共識。現(xiàn)在有一個詳細的過程，用于使用 SPARK 來滿足 DO-333/ED-216 的目標(biāo)，作為某些形式的測試的替代品，重點是檢查源代碼是否一致、準確并符合低級要求。

該過程解決了使用正式方法時的替代覆蓋目標(biāo)以及源代碼和可執(zhí)行目標(biāo)代碼之間的財產(chǎn)保護目標(biāo)。當(dāng)某些測試被使用正式方法所取代時，前者是必需的。后者是必需的，以便從可執(zhí)行目標(biāo)代碼的源代碼驗證中受益。已與美國聯(lián)邦航空管理局（FAA）和歐洲航空安全局（EASA）討論了此過程，以便將來在DO-178C / ED-12C中使用SPARK的申請人。

航空電子學(xué)中的形式化方法

盡管在DO-178的C版中添加正式方法補充是2012年，但使用正式方法開發(fā)航空電子軟件至少可以追溯到1990年代，當(dāng)時John Rushby寫了一份關(guān)于它們用于FAA的全面指導(dǎo)文件。［“形式方法和關(guān)鍵系統(tǒng)的認證”，拉什比，F(xiàn)AA，1993年。雖然Rushby專注于演繹方法，但從那時起自動化和計算機能力的提高使得另外兩種形式化方法對開發(fā)航空電子軟件具有吸引力：模型檢查和抽象解釋。DO-333專門針對使用這三類形式化方法來開發(fā)航空電子軟件。美國宇航局2014年的一份報告中介紹了所有三個類別的使用示例［“DO-333認證案例研究”，Cofer和Miller，Rockwell Collins，2014年。

圖1：DO-333 驗證活動。圖形由IEEE提供。

雖然抽象解釋和模型檢查非常適合以最少的人為干預(yù)檢查代碼庫中的簡單程序?qū)傩裕鼈儠龅剿^的狀態(tài)爆炸問題，當(dāng)分析的模型的大小（無論是在模型檢查中顯式提供還是由工具從抽象解釋構(gòu)建）太大而無法完成分析時。演繹方法沒有這些缺點，但它們有要求用戶編寫函數(shù)合約的成本。這些協(xié)定是函數(shù)行為的（部分）規(guī)范，既定義了驗證目標(biāo)，也定義了用于分析對該函數(shù)的調(diào)用的函數(shù)行為的適當(dāng)摘要。這允許演繹方法應(yīng)用強大的驗證技術(shù)，這些技術(shù)可以證明軟件的非平凡屬性，因為函數(shù)合約使焦點能夠?qū)Ｗ⒂趯蝹€函數(shù)的驗證，一次一個。

兩個工具集為C和Ada的工業(yè)用戶提供基于演繹方法的形式程序驗證：用于C程序的Frama-C工具集和用于Ada程序的SPARK工具集。兩者都被用于DO-178航空電子設(shè)備認證。例如，洛克希德馬丁公司最初在1997年將SPARK用于C-130J美國軍方和英國皇家空軍飛機的控制軟件。此后，BAE系統(tǒng)公司使用SPARK在維護期間證明了C-130J控制軟件的關(guān)鍵特性。另一個例子，在DO-333中記錄，空中客車公司在2002年使用Caveat（Frama-C的前身）來證明對空中客車A380民用飛機的低級要求，作為單元測試的替代品。

B. 所處理的核查目標(biāo)

SPARK 可用作 DO-333 中許多驗證目標(biāo)的主要證據(jù)來源，從低級要求 （LLR） 到源代碼和可執(zhí)行目標(biāo)代碼 （EOC）。形式驗證是分析的一個特殊情況，因此將形式分析應(yīng)用于LLR和源代碼所需的指導(dǎo)只是使用形式分析的標(biāo)準和條件。［“在認證環(huán)境中使用形式方法的指南”，Brown 等人，SC-205/WG-71，ERTS 2010。在EOC中使用需要更多的理由，特別是在替換單元測試時。

當(dāng) LLR 在 SPARK 中表示為合約時，正式符號保證 LLR 是精確和明確的，因此準確性是有保證的。一致性也得到了保證，因為不同功能的合同不會沖突。合約也是可驗證的，并且通過設(shè)計符合（編程語言）標(biāo)準。這些包括表FM的目標(biāo)2、4和5。來自DO-4的A-333。（同前科弗和米勒。

SPARK 的主要資源之一是它自動顯示源代碼符合以函數(shù)契約表示的 LLR。函數(shù)協(xié)定還可以表達數(shù)據(jù)依賴關(guān)系，SPARK 工具集可以自動顯示源代碼符合軟件體系結(jié)構(gòu)的這一部分。SPARK代碼是可驗證的，并且符合（編程語言）標(biāo)準的設(shè)計。函數(shù)的源代碼隱式追溯到函數(shù)協(xié)定中表示的 LLR。最后，SPARK 代碼是明確的，因此可以自動分析源代碼的一致性，以表明它沒有未初始化數(shù)據(jù)的讀取、算術(shù)溢出、其他運行時錯誤和未使用的計算（變量、語句等）。這些指標(biāo)包括表FM的目標(biāo)1至6。來自DO-5的A-333。

平機會在LLR方面的合規(guī)性和穩(wěn)健性的目標(biāo)（表FM的目標(biāo)3和4。DO-333的A-6）可以通過依賴源代碼的相應(yīng)目標(biāo)來解決，前提是同時提供源代碼和EOC之間的財產(chǎn)保護演示。顯示財產(chǎn)保全的一種方法是合理地證明，在所有可能的情況下，編譯器都保留了從源代碼到EOC的程序語義。不幸的是，似乎沒有任何合理的辦法能夠提供這種信心。通過在SPARK中執(zhí)行合約的模式下運行集成測試，用戶可以確信編譯器在EOC中正確保留了源代碼的語義;否則，在單個函數(shù)中證明的合同將在集成測試中（很有可能）失敗。通過在執(zhí)行和不執(zhí)行合約的情況下運行集成測試并檢查輸出是否相同，用戶可以確信合約的編譯不會影響代碼的編譯，因為否則在某些測試中輸出很可能會有所不同。

當(dāng)然，使用 SPARK 的一個主要好處是能夠通過 SPARK 分析替換單元測試。在這種情況下，DO-333還定義了表FM的附加目標(biāo)5至8。A-7.正式驗證和審查的結(jié)合可以實現(xiàn)這些目標(biāo)，正如空中客車和達索航空過去的經(jīng)驗所證明的那樣。［“測試或形式驗證：DO-178C 替代方案和工業(yè)”，Moy 等人，IEEE Software 2013。這里使用了 SPARK 的幾個功能，例如在函數(shù)契約中聲明數(shù)據(jù)依賴關(guān)系的能力，以及通過不相交的情況表達函數(shù)契約的可能性。

即將上來

自 1990 年代以來，一些先驅(qū)者一直在使用正式的程序驗證工具集。航空電子軟件認證中正式程序驗證自動化的進展現(xiàn)在使更多公司可以使用這些技術(shù)。SPARK使用戶能夠解決DO-178C的形式方法補充DO-333中定義的許多驗證目標(biāo)。美國和歐洲的認證機構(gòu)現(xiàn)在正在看好在航空電子認證中使用這種方法的申請人。

審核編輯：郭婷