您能以多快的速度將軟件推出并準(zhǔn)備好？

長(zhǎng)期以來(lái)，這個(gè)單一的問(wèn)題推動(dòng)了大部分嵌入式工業(yè)行業(yè)。按時(shí)發(fā)布此年度版本，滿足該功能里程碑。只要軟件功能相對(duì)簡(jiǎn)單或次于系統(tǒng)功能，就可以了。

但隨著系統(tǒng)復(fù)雜性和互連性的日益增加，曾經(jīng)是良性的小故障或“故障”現(xiàn)在正在造成威脅，有時(shí)甚至危及人的生命。無(wú)人機(jī)、自動(dòng)駕駛汽車和醫(yī)療設(shè)備是這一趨勢(shì)的三個(gè)非常重要的代表。那么問(wèn)題就不再是軟件能否按時(shí)交付，而是正確、安全、可靠的軟件能否及時(shí)交付。這是一個(gè)完全不同的野獸。

除了驗(yàn)證它正在做它應(yīng)該做的事情之外，沒(méi)有太多可以做的事情來(lái)交付正確的軟件。不幸的是，傳統(tǒng)的軟件開發(fā)方法并不是為了簡(jiǎn)化正式規(guī)范或優(yōu)化驗(yàn)證成本而設(shè)計(jì)的。而且越晚檢測(cè)到問(wèn)題，修復(fù)的成本就越高，以至于在第一天需要幾分鐘才能解決的問(wèn)題可能會(huì)在集成過(guò)程中持續(xù)數(shù)月。是的，使用傳統(tǒng)語(yǔ)言和環(huán)境編寫極其強(qiáng)大的軟件是可能的，但成本高得離譜。

特別是對(duì)于在微控制器 （MCU） 上運(yùn)行的嵌入式應(yīng)用程序，一個(gè)更加復(fù)雜的因素是編寫測(cè)試的難度。當(dāng)涉及低級(jí)嵌入式功能時(shí)，編寫甚至運(yùn)行廣泛的測(cè)試活動(dòng)可能是不切實(shí)際的。任何可以在這些程序之前幫助清除問(wèn)題或確保正確性的東西都可以節(jié)省大量成本。

另一方面，從一開始就利用表達(dá)性和正式的規(guī)范，使實(shí)施者更容易尊重需求，提供自動(dòng)驗(yàn)證，從而防止問(wèn)題或在開發(fā)周期的早期發(fā)現(xiàn)問(wèn)題。

Ada 和 SPARK 語(yǔ)言在這方面提供了獨(dú)特的解決方案，將規(guī)范、編碼和驗(yàn)證集成到一個(gè)通用的形式中。這些語(yǔ)言的核心原則是在軟件級(jí)別盡可能多地指定，以便在實(shí)現(xiàn)時(shí)可以驗(yàn)證盡可能多的組件。

下面逐步檢查實(shí)際的 Ada 或 SPARK 實(shí)現(xiàn)。

規(guī)格

在將 Ada 和 SPARK 語(yǔ)言與替代語(yǔ)言進(jìn)行比較時(shí)，突出的一件事是可以添加到軟件源代碼中以捕獲除實(shí)際功能之外的約束和意圖的信息量。數(shù)據(jù)類型不僅僅是一個(gè)整數(shù)或浮點(diǎn)數(shù)：它是一個(gè)語(yǔ)義實(shí)體，可以與一組有效值、一組操作、最小精度、內(nèi)存表示，甚至物理維度相關(guān)聯(lián)。同樣，函數(shù)不僅僅是一種從參數(shù)計(jì)算值的方法：它有一組可以調(diào)用的條件，在它返回時(shí)提供一組保證，并對(duì)它的環(huán)境（參數(shù)和全局變量）產(chǎn)生影響）。

Ada 和 SPARK 有很多特性可以用來(lái)豐富規(guī)范，但是為了本文的目的，我們選擇一個(gè)例子：

這個(gè)簡(jiǎn)單的過(guò)程在其屬性和行為方面揭示了很多：

首先，C 是一個(gè)in out參數(shù)，所以它必須在被調(diào)用之前被初始化，并且它的值在子程序中被修改。請(qǐng)注意，沒(méi)有指示它是通過(guò)復(fù)制還是引用傳遞，這是由編譯器根據(jù)語(yǔ)言約束和效率自動(dòng)決定的。

E 是輸入?yún)?shù)，或不打算修改的輸入值。一個(gè)前提條件是在調(diào)用之前容器未滿。就設(shè)計(jì)而言，這是一個(gè)極其重要的轉(zhuǎn)變，就像在其他語(yǔ)言中的Push過(guò)程可能負(fù)責(zé)檢測(cè)錯(cuò)誤的調(diào)用上下文（如果容器已滿）并實(shí)施緩解技術(shù)（或防御性代碼）。另一方面，使用先決條件，該過(guò)程可以安全地假設(shè)容器未滿（否則它會(huì)被靜態(tài)或動(dòng)態(tài)檢測(cè)到，但稍后會(huì)詳細(xì)介紹）并避免這些額外的代碼。驗(yàn)證輸入的責(zé)任隱含在調(diào)用者身上，然后調(diào)用者可以將其提升給自己的調(diào)用者，直到到達(dá)代碼中數(shù)據(jù)驗(yàn)證確實(shí)有意義的地方。

后置條件提供了有關(guān)過(guò)程行為的關(guān)鍵屬性——這里，E 包含在修改后的容器中并且計(jì)數(shù)增加的事實(shí)。

查看與嵌入式開發(fā)相關(guān)的一些約束，另一個(gè)有用的方面是指定內(nèi)存映射約束。Ada 允許聲明式表示法來(lái)指定數(shù)據(jù)結(jié)構(gòu)在內(nèi)存中的布局方式和地址，從而避免容易出錯(cuò)的按位操作和一致性檢查。例如：

上面聲明了一個(gè)數(shù)據(jù)結(jié)構(gòu)以及一些與邊界相關(guān)的字段：

數(shù)據(jù)的大小固定為 16 位，接下來(lái)的兩個(gè)方面（具有值High_Order_First）基本上告訴編譯器使用大端表示。

下一個(gè)子句提供特定的位表示（例如，Size從索引位1到4的字節(jié)0開始。

最后，為R提供了它在內(nèi)存中的地址。

實(shí)施（在 SPARK/Ada 或 C 中）

Ada 和 SPARK 語(yǔ)言提供了現(xiàn)代命令式語(yǔ)言的大部分功能。這些功能如何實(shí)現(xiàn)的最顯著特性是它們?yōu)榫幾g器解釋提供的空間很小并且避免了捷徑。例如，沒(méi)有隱式轉(zhuǎn)換，并且輕松地執(zhí)行指針運(yùn)算之類的操作需要 5 行代碼。但是，在實(shí)際編碼階段花費(fèi)的額外時(shí)間很容易通過(guò)易于驗(yàn)證來(lái)重新獲得，無(wú)論是用于代碼閱讀、測(cè)試還是靜態(tài)分析。

在討論的這一點(diǎn)上，值得一提的是房間里的大象：對(duì)于新開發(fā)的代碼來(lái)說(shuō)，使用一種新語(yǔ)言可能是一個(gè)好主意，但通常存在一個(gè)不容忽視的預(yù)先存在的環(huán)境。這通常是來(lái)自其他項(xiàng)目或現(xiàn)成庫(kù)的代碼。這段代碼可能是用 C 語(yǔ)言或 C++ 創(chuàng)建的。僅此一項(xiàng)就經(jīng)常驅(qū)動(dòng)開發(fā)語(yǔ)言的選擇。

幸運(yùn)的是，SPARK 和 Ada 已被設(shè)計(jì)為與 C 環(huán)境很好地集成。一些指令可以將 C 直接映射到 Ada，反之亦然，而無(wú)需任何包裝代碼的開銷。這種映射甚至可以自動(dòng)生成。

因此，如果不推薦的話，在 SPARK 或 Ada 中僅開始開發(fā)幾個(gè)組件，而在其他情況下保留在 C 環(huán)境中是完全合理的。

目前可用于 Ada 和 SPARK 的主要編譯器技術(shù)是 GCC，但也可以提供其他編譯器技術(shù)。這意味著 SPARK 和 C 代碼可以使用相同的技術(shù)進(jìn)行編譯，具有相同的優(yōu)化和代碼生成通道。結(jié)果，C 和 SPARK 代碼之間的性能幾乎沒(méi)有差異，并且沒(méi)有從一種語(yǔ)言到另一種語(yǔ)言的控制流的損失。

談到我們之前的一個(gè)例子，讓我們假設(shè)正在使用一個(gè)用 C 實(shí)現(xiàn)的容器。我們?cè)噲D與之交互的 C 代碼如下所示：

除了來(lái)自 C 的實(shí)現(xiàn)聲明之外，規(guī)范在 Ada/SPARK 中完全相同。

Ada 或 SPARK 代碼可以像在 Ada 中實(shí)現(xiàn)一樣使用此過(guò)程。與導(dǎo)入類似，導(dǎo)出允許 C 調(diào)用用 Ada 編寫的子程序。如果需要，這些接口層可以通過(guò)綁定生成器自動(dòng)生成。

盡管將 SPARK 和 C 一起編譯解決了許多用例，但仍然存在最終代碼必須是 C 的情況。確實(shí)，一些用戶雖然對(duì)使用 SPARK 進(jìn)行開發(fā)感興趣，但仍需要將 C 代碼交付給他們的客戶。

可以使用一個(gè)特殊的編譯器來(lái)覆蓋這個(gè)用例，即“GNAT 通用代碼生成器”。它本質(zhì)上將 Ada 語(yǔ)言的一個(gè)子集編譯為 C。借助這項(xiàng)技術(shù)，SPARK 幾乎成為一種建模語(yǔ)言，其輸出集成在 C 環(huán)境中。它也可以被視為一種交付形式驗(yàn)證的 C 代碼的方式，驗(yàn)證在 SPARK 級(jí)別執(zhí)行。

在數(shù)據(jù)表示示例（寄存器案例）中，在代碼中使用這段數(shù)據(jù)非常簡(jiǎn)單。分配一個(gè)值如下所示：

這里不需要按位運(yùn)算，因?yàn)榫幾g器會(huì)在后臺(tái)自動(dòng)生成適當(dāng)?shù)拇a。

確認(rèn)

Ada 和 SPARK 在源代碼中提供了大量信息，可供各種檢查器使用。例如，作為第一道防線，編譯器將檢測(cè)到許多不一致之處，并可以在測(cè)試階段自動(dòng)在可執(zhí)行文件中插入動(dòng)態(tài)驗(yàn)證。有了這個(gè)級(jí)別的信息，就可以超越經(jīng)典的靜態(tài)分析并應(yīng)用程序驗(yàn)證技術(shù)來(lái)演示整個(gè)應(yīng)用程序的屬性。

對(duì)于較低級(jí)別的數(shù)據(jù)結(jié)構(gòu)，也會(huì)進(jìn)行自動(dòng)一致性驗(yàn)證。編譯器驗(yàn)證特定大小是否足以實(shí)現(xiàn)所需的數(shù)據(jù)范圍，沒(méi)有數(shù)據(jù)重疊等。此外，形式證明可用于驗(yàn)證分配的值是否始終在任何分配的范圍內(nèi)。

繼續(xù)前面的另一個(gè)示例，假設(shè)在我們想要驗(yàn)證的一段代碼中調(diào)用了Push 。例如，我們可以讓以下語(yǔ)句從輸入文件中讀取數(shù)字，直到它達(dá)到 0：

這個(gè)Push調(diào)用將被 SPARK 工具標(biāo)記為不正確，因?yàn)闊o(wú)法知道循環(huán)不會(huì)達(dá)到容器 C 的最大容量。證明者無(wú)法證明Push的前提條件，這顯然應(yīng)該在調(diào)用，而不是在被調(diào)用的過(guò)程中。如果到達(dá)文件末尾而沒(méi)有擊中0 ，則示例代碼中可能會(huì)出現(xiàn)另一個(gè)潛在錯(cuò)誤。如果指定了適當(dāng)?shù)南葲Q條件，證明者將能夠判斷循環(huán)中缺少檢查以驗(yàn)證是否仍需要讀取輸入。

這種問(wèn)題通常會(huì)在某個(gè)時(shí)候發(fā)生。如果覆蓋極端案例的單元測(cè)試足夠廣泛，那么問(wèn)題將在該級(jí)別得到解決。然而，當(dāng)真正的數(shù)據(jù)開始輸入系統(tǒng)時(shí)，他們可以找到自己的方式進(jìn)行集成測(cè)試，或者當(dāng)用戶試圖破壞系統(tǒng)時(shí)進(jìn)行 beta 測(cè)試。在最壞的情況下，其中一些錯(cuò)誤會(huì)通過(guò)部署找到并需要在客戶報(bào)告后進(jìn)行追蹤。問(wèn)題不是它們是否會(huì)被發(fā)現(xiàn)，而是當(dāng)它們被發(fā)現(xiàn)時(shí)修復(fù)它們的成本會(huì)有多高。越晚發(fā)現(xiàn)，越多的人參與到鏈條中，需要更多的調(diào)查來(lái)確定源頭、修復(fù)問(wèn)題、證明修復(fù)的合理性、測(cè)試修復(fù)、重新交付產(chǎn)品等。使用技術(shù)早期集成驗(yàn)證 - 在這種情況下，

舊的又是新的

Ada 和 SPARK 方法的獨(dú)特之處在于它集成了軟件規(guī)范、實(shí)現(xiàn)和驗(yàn)證，提供了一種以現(xiàn)代系統(tǒng)所需的完整性級(jí)別生產(chǎn)軟件的經(jīng)濟(jì)高效的方法。醫(yī)療、汽車和工業(yè)物聯(lián)網(wǎng) （IIoT） 等行業(yè)一直在尋找傳統(tǒng) C 語(yǔ)言開發(fā)的替代方案，Ada 和 SPARK 提供了經(jīng)過(guò)驗(yàn)證的解決方案。

作為 Ada 語(yǔ)言的提供者，AdaCore 在過(guò)去幾年中觀察到對(duì)該技術(shù)的新興趣。今天的限制提供了一個(gè)嘗試新事物的好機(jī)會(huì)——或者正在卷土重來(lái)的舊事物。

審核編輯：郭婷