操作應用于安全苛刻的航空和軍事領(lǐng)域的嵌入式軟件時必須高度關(guān)注安全問題。為達到可靠性目標，軟件開發(fā)團隊精益求精，力爭使這些軟件應用符合嚴格的驗證流程并實現(xiàn)零缺陷目標。Edsger Dijkstra有句名言：測試只能發(fā)現(xiàn)錯誤，但不能證明錯誤不存在。如果測試無法證明不存在嚴重的運行錯誤，那么嵌入式軟件開發(fā)團隊如何才能確定其軟件沒有這些錯誤呢?基于數(shù)學證明的代碼驗證是值得一試的解決方案。在軟件驗證方面，可擴展的高性能數(shù)學技術(shù)在實際應用方面的最新發(fā)展十分有用，可實現(xiàn)對軟件中不存在運行時錯誤進行證明。

　　航空領(lǐng)域的軟件應用

　　高集成系統(tǒng)中的嵌入式軟件日益復雜。在軍事領(lǐng)域中，用于F-22猛禽戰(zhàn)斗機的航空電子軟件由170萬行代碼組成，用于F-35聯(lián)合攻擊戰(zhàn)斗機的航空電子軟件預計有570萬行代碼。對于商務班機，波音787飛機飛行控制系統(tǒng)將有大約650萬行代碼。軟件內(nèi)容不斷膨脹，飛機復雜性不斷增加，使發(fā)生故障的風險也不斷加劇，從而使獲得高度可信性軟件的過程復雜無比。

　　軟件故障風險

　　研究以往發(fā)生的嵌入式設(shè)備故障對于理解代碼相關(guān)的問題大有裨益。例如，一次性使用火箭在測試飛行期間發(fā)生的故障歸根于代碼缺陷。在這種特殊情況下，發(fā)射器在發(fā)射后不到一分鐘的時間內(nèi)自毀，原因在于：攻角超過規(guī)定的安全限度，導致發(fā)射器遭遇高氣動載荷。

　　事后調(diào)查揭露了故障的根本原因：溢出導致嵌入式軟件發(fā)生運行錯誤。在將一個64位浮點數(shù)轉(zhuǎn)換為16位有符號整數(shù)時，一對決定火箭姿態(tài)和位置的冗余慣性參考系統(tǒng)中產(chǎn)生溢出，從而將火箭噴管移到了極端位置。冗余系統(tǒng)的存在不起作用，因為備用系統(tǒng)也發(fā)生了同樣的問題。

　　如上所述的運行時錯誤代表一類特定的軟件錯誤，稱作潛伏性故障。這類故障位于代碼中，但是除非在特殊條件下運行特定測試，否則在系統(tǒng)測試期間無法檢測到這些故障。因此，這些代碼表面上能正常運行，但實際上會導致意外的系統(tǒng)故障。以下為若干運行時錯誤示例：數(shù)據(jù)未初始化;數(shù)組訪問越界;空指針解引用;溢出和下溢;計算錯誤;同時訪問共享數(shù)據(jù);非法類型轉(zhuǎn)換。

　　高集成軟件驗證

　　按照傳統(tǒng)方法，源代碼級軟件驗證涉及代碼檢查、靜態(tài)分析和動態(tài)測試。每種方法都有缺點。

　　代碼檢查僅依賴于檢察人員的專業(yè)技術(shù)，若有大量代碼需要檢查，則會是一項繁瑣的工作。傳統(tǒng)的靜態(tài)分析技術(shù)主要依靠模式匹配方法檢測不安全的代碼模式，但無法證明不存在運行時錯誤。隨著嵌入式軟件日益復雜，對所有操作條件進行動態(tài)測試已經(jīng)不太可能，這進一步證明了Edsger Dijkstra的觀點：測試只能發(fā)現(xiàn)錯誤，但不能證明錯誤不存在。

　　一種新的驗證方法稱為抽象解釋，它以靜態(tài)分析為基礎(chǔ)，使用形式化數(shù)學證明，可發(fā)現(xiàn)某些運行時錯誤或證明它們不存在。抽象解釋可直接應用于源代碼，而無需執(zhí)行代碼。

　　抽象解釋和基于證明的驗證方法作為一種基于證明的驗證方法，通過在以下問題中將三個大整數(shù)相乘可對抽象解釋進行說明：–4586×34985×2389=?

　　雖然手動計算此問題的答案很費時，但是我們可以應用乘法法則確定答案的符號為負。確定此計算的符號就是抽象解釋的一種應用。這種技巧使我們不需要對整數(shù)執(zhí)行完成的乘法計算就能夠準確地知道最終結(jié)果的一些屬性，例如符號。利用乘法法則，我們還知道此計算的結(jié)果符號不可能為正。采用類似方式可將抽象解釋應用到軟件符號學中，以證明軟件的某些屬性。不執(zhí)行程序本身，

　　通過驗證源代碼的某些動態(tài)屬性，抽象解釋在傳統(tǒng)靜態(tài)分析技術(shù)和動態(tài)測試之間架起橋梁。抽象解釋在單個階段中調(diào)查程序的所有可能行為，即所有可能值的組合，以確定如何以及在何種條件下程序會產(chǎn)生某些類別的運行時故障。由于抽象解釋與考慮中的操作相關(guān)，我們可以用數(shù)學方法證明該技術(shù)能預測正確的結(jié)果，因此它得出的結(jié)果被認為是可靠的。

　　使用抽象解釋驗證軟件

　　抽象檢查可用作靜態(tài)分析工具，檢測并用數(shù)學方法證明源代碼中不存在某些運行時錯誤，如溢出、除以零以及數(shù)組訪問超出邊界等。執(zhí)行此驗證無需執(zhí)行程序、代碼插裝或測試用例。MathWorks Polyspace代碼驗證產(chǎn)品使用的便是此類靜態(tài)分析。向Polyspace產(chǎn)品輸入C、C++或Ada源代碼。Polyspace產(chǎn)品首先檢查源代碼，以確定可能出現(xiàn)潛在運行時錯誤的位置。然后它會生成一份報告，該報告使用顏色編碼表示代碼中各元素的狀態(tài)，如圖1和表1所示。

　　圖1 Polyspace顏色編碼

　　表1：顏色編碼

　　標為綠色的Polyspace結(jié)果表示代碼中不存在某些運行時錯誤。在檢測到運行時錯誤且代碼顯示為紅色、灰色或橙色的情況下，軟件開發(fā)人員和測試人員可使用驗證流程中生成的信息修復發(fā)現(xiàn)的運行時錯誤。

　　結(jié)論

　　靜態(tài)分析融合抽象解釋后，可提高高集成系統(tǒng)中嵌入式軟件的質(zhì)量和可靠性。此方法能幫助工程師實現(xiàn)證明軟件中不存在某些運行時錯誤的目標。具有抽象解釋的代碼驗證解決方案有助于實現(xiàn)良好的質(zhì)量流程。這是強有力的驗證流程，可幫助實現(xiàn)嵌入式設(shè)備的高集成性。