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

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

穩(wěn)健：

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

對代碼的適用性：

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

普通工程師的可用性：

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

改進測試：

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

可認證性：

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

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

審核編輯：郭婷