雖然 Ada 提供了許多在運(yùn)行時(shí)充當(dāng)安全防護(hù)的功能，但在檢測(cè)到違規(guī)時(shí)會(huì)引發(fā)異常，但其中一些功能可能過于復(fù)雜，無法保證在程序運(yùn)行之前安全執(zhí)行。例如指針就是這種情況，指針可用于在內(nèi)存中創(chuàng)建任意復(fù)雜的共享數(shù)據(jù)結(jié)構(gòu)。SPARK 是 Ada 的一個(gè)子集，它禁止這些功能，最明顯的是指針，以便能夠在編譯時(shí)提供強(qiáng)有力的保證。SPARK的下一個(gè)修訂版SPARK 2014的預(yù)覽版以及相關(guān)的驗(yàn)證工具已經(jīng)可用。

盡管SPARK的演進(jìn)一直伴隨著Ada的演進(jìn)，每個(gè)新版本的Ada（SPARK 83，SPARK 95，SPARK 2005）都有一個(gè)新版本的SPARK，但新版本SPARK 2014在許多方面都有很大的不同。SPARK 2014 是 2010年啟動(dòng)的一個(gè)項(xiàng)目的結(jié)果，該項(xiàng)目旨在使使用形式驗(yàn)證而不是測(cè)試關(guān)鍵軟件具有成本效益。就在幾個(gè)月前，空中客車公司提出了采用正式方法的五個(gè)“必備”標(biāo)準(zhǔn)：健全性，代碼的適用性，“普通”工程師在“普通”計(jì)算機(jī)上的可用性，對(duì)經(jīng)典方法的改進(jìn)，可認(rèn)證性。在這三年中，我們非常牢記這五個(gè)標(biāo)準(zhǔn)，以下是SPARK 2014和相關(guān)驗(yàn)證工具GNATprove的結(jié)果。

穩(wěn)?。?/p>

這是語言和工具的基石。它不僅限于說：“我們使用霍爾邏輯”。我們想要實(shí)現(xiàn)的是“最大”的健全性：當(dāng)你適當(dāng)?shù)厥褂盟鼈儠r(shí)，不僅工具不能陳述錯(cuò)誤的屬性，而且通過濫用工具（例如通過陳述錯(cuò)誤的公理）來獲得對(duì)軟件的錯(cuò)誤信心也不容易。為了確保最大的合理性，采取了許多決定，例如禁止用戶陳述公理。

對(duì)代碼的適用性：

SPARK 2014 是 Ada 的最大可能子集，它仍然可以進(jìn)行形式驗(yàn)證。特別是，它包括泛型、標(biāo)記類型、判別器、動(dòng)態(tài)類型、早期回報(bào)以及 SPARK 2005 中排除的許多其他功能。對(duì)于代碼中無法正式分析的部分，我們已經(jīng)可以將形式驗(yàn)證與測(cè)試結(jié)合起來。因此，它不是一種全有或全無的技術(shù)，而是您可以在任何Ada項(xiàng)目中真正引入的技術(shù)。

普通工程師的可用性：

這是這些年來讓我們最忙的問題。首先，我們已經(jīng)實(shí)現(xiàn)了自動(dòng)化水平，大多數(shù)證明都是自動(dòng)通過的，特別是沒有運(yùn)行時(shí)錯(cuò)誤的證明。其次，我們將工具緊密集成到開發(fā)人員工作流（例如，通過使用項(xiàng)目文件和自動(dòng)計(jì)算的依賴項(xiàng)）和開發(fā)環(huán)境（例如，在特定子程序或代碼行上運(yùn)行GNATprove 的能力，以及顯示有問題的程序路徑）。

改進(jìn)測(cè)試：

形式驗(yàn)證是詳盡無遺的，這一事實(shí)使其成為關(guān)鍵軟件所要求的昂貴單元測(cè)試活動(dòng)的理想替代品。這方面的主要挑戰(zhàn)是促進(jìn)逐步采用正式核查。由于形式驗(yàn)證所需的子程序合同對(duì)于測(cè)試已經(jīng)很有用，并且由于GNATproly可以單獨(dú)應(yīng)用于任何Ada程序中的各個(gè)SPARK子程序，因此切換到形式驗(yàn)證可以在幾天內(nèi)完成。

可認(rèn)證性：

當(dāng)我們開始這個(gè)項(xiàng)目時(shí)，航空電子標(biāo)準(zhǔn)DO-178的正式方法補(bǔ)充尚未最終確定。從那時(shí)起，它與新版本的標(biāo)準(zhǔn)DO-178C一起發(fā)布，因此今天，GNATprove 可以用于代替在最高級(jí)別A或B開發(fā)的平面中測(cè)試關(guān)鍵嵌入式程序。我們?cè)贗EEE軟件上發(fā)表了一篇關(guān)于如何處理在這種情況下覆蓋的微妙問題的論文。當(dāng)然，已經(jīng)認(rèn)可形式化方法的其他領(lǐng)域的項(xiàng)目（例如鐵路）也可以使用GNATprove。

該項(xiàng)目開發(fā)的工業(yè)案例研究的結(jié)果是公開的，供其他人了解新技術(shù)擅長(zhǎng)什么以及當(dāng)前發(fā)展階段。當(dāng)用戶從以前的SPARK技術(shù)切換到新的SPARK 2014技術(shù)時(shí)，最常見的評(píng)論可能是執(zhí)行規(guī)范的能力提供了令人難以置信的可用性改進(jìn)。這種動(dòng)態(tài)技術(shù)和靜態(tài)技術(shù)的結(jié)合對(duì)于軟件驗(yàn)證的未來無疑是有希望的。

審核編輯：郭婷