航空電子認(rèn)證中的正式程序驗(yàn)證

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

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

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

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

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

圖1：DO-333 驗(yàn)證活動(dòng)。圖形由IEEE提供。

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

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

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

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

當(dāng) LLR 在 SPARK 中表示為合約時(shí)，正式符號(hào)保證 LLR 是精確和明確的，因此準(zhǔn)確性是有保證的。一致性也得到了保證，因?yàn)椴煌δ艿暮贤粫?huì)沖突。合約也是可驗(yàn)證的，并且通過設(shè)計(jì)符合（編程語言）標(biāo)準(zhǔn)。這些包括表FM的目標(biāo)2、4和5。來自DO-4的A-333。（同前科弗和米勒。

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

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

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

即將上來

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

審核編輯：郭婷