DO-332是DO-178C標(biāo)準(zhǔn)對面向?qū)ο蠹夹g(shù)（OOT）和相關(guān)技術(shù)的補(bǔ)充，分析了安全關(guān)鍵軟件中面向?qū)ο笠l(fā)的問題，并為處理OOT的漏洞提供了新的指導(dǎo)。DO-332的一個重要新目標(biāo)是“本地類型一致性驗證”，它利用了稱為“Liskov替換原理”的類型理論結(jié)果，并幫助解決OOT的動態(tài)靈活性帶來的一些關(guān)鍵認(rèn)證挑戰(zhàn)。

面向?qū)ο蠹夹g(shù)（OOT）被廣泛使用，并得到包括C++，Java和Ada在內(nèi)的一系列編程語言的支持，但由于各種原因，它的普及尚未擴(kuò)展到機(jī)載和其他安全關(guān)鍵軟件。根本問題是驗證利用OOT三個基本元素的軟件的復(fù)雜性：繼承，多態(tài)性和動態(tài)綁定。（圖 1 說明了面向?qū)ο蟮幕A(chǔ)知識。一個簡單的例子說明了這些問題：

圖1：面向?qū)ο蠡A(chǔ)知識

假設(shè) Sensor 類是繼承層次結(jié)構(gòu)的根，ref 是對此層次結(jié)構(gòu)中任何類中的對象的多態(tài)引用，而 Reset 是為不同的 Sensor 類定義不同的操作。聲明參考。Reset（。..） 根據(jù) ref 表示的對象的類動態(tài)綁定到相應(yīng)的版本。如何驗證此調(diào)用是否滿足重置操作的要求？

如果使用繼承來定義不是傳感器專用化的子類，則會出現(xiàn)一個問題。此子類的重置可能具有與重置傳感器無關(guān)的某些效果，或者可能會生成異常。ref 從這樣的子類引用對象將是一個錯誤，需要分析以表明錯誤不會發(fā)生。這使驗證過程復(fù)雜化。

另一個問題涉及結(jié)構(gòu)覆蓋率分析。對于 DO-178 標(biāo)準(zhǔn)中三個最高級別（A、B 或 C）中的任何一個的系統(tǒng)，必須使用基于需求的測試來證明完整的語句覆蓋率。但是，編譯器可能會選擇幾種實(shí)現(xiàn)策略來處理動態(tài)綁定，這些策略對“語句覆蓋率”的含義有不同的含義。結(jié)構(gòu)覆蓋范圍的范圍不應(yīng)取決于編譯器使用的實(shí)現(xiàn)策略。

DO-332［1］是DO-178C［2］的OOT補(bǔ)充，通過局部類型一致性的新概念解決了這些問題，該概念利用了繼承只應(yīng)用于類專用化的原則。

繼承和利斯科夫替代原則

在面向?qū)ο蟮脑O(shè)計中，系統(tǒng)的體系結(jié)構(gòu)反映了類及其關(guān)系。一個特別重要的關(guān)系是專業(yè)化（“is a”），但還有很多其他關(guān)系。實(shí)現(xiàn)設(shè)計涉及選擇用于捕獲關(guān)系的語言機(jī)制。

在面向?qū)ο蟮恼Z言中，繼承可用于實(shí)現(xiàn)兩個類之間的各種關(guān)系。但是，當(dāng)繼承用于專用化以外的任何內(nèi)容時，可能會出現(xiàn)異常，因為為超類定義的操作可能對子類沒有意義。在類型論的背景下，已經(jīng)研究了將繼承限制為專業(yè)化關(guān)系，其中它被稱為Liskov替換原理（LSP）［3］。非正式地說，LSP 意味著無論在哪里可以使用超類的實(shí)例，都應(yīng)該允許替換任何子類的實(shí)例。

使用繼承進(jìn)行專業(yè)化與操作的前置條件和后置條件（其“協(xié)定”）具有重要的交互作用。前提條件是在調(diào)用操作時對程序狀態(tài)所做的假設(shè)。后置條件是保證操作在操作完成時對程序狀態(tài)進(jìn)行的操作。前置和后置條件可以明確指定 - 可以在源文本中指定，如Ada 2012［4］或SPARK［5］，也可以單獨(dú)指定 - 或者它們可以隱含在操作邏輯中。

如果繼承符合 LSP，則操作的子類版本不應(yīng)施加比超類版本更強(qiáng)（更具限制性）的前提條件。否則，調(diào)用可能在某些情況下（在超類實(shí)例上）成功，但在其他情況下（在子類實(shí)例上）失敗。類似地，子類的操作版本不應(yīng)指定比超類版本更弱（更通用）的后置條件。

因此，符合 LSP 意味著滿足兩個屬性：

協(xié)定一致性：任何子類操作都不會加強(qiáng)它所覆蓋的超類操作的前置條件或削弱后置條件。

行為一致性：每個子類操作都滿足其超類的要求。

DO-332 在新目標(biāo)“本地類型一致性驗證”中捕獲了這些概念。此目標(biāo)不需要證明類層次結(jié)構(gòu)符合 LSP，這將過于嚴(yán)格。相反，它反映了對于符合要求的類體系結(jié)構(gòu)，驗證工作更簡單，并且分析只需要考慮本地上下文。

本地類型一致性

圖 2 顯示了與驗證本地類型一致性相關(guān)的活動，DO-332 需要 A、B 或 C 級別的軟件。“對于使用替換的每個子類型”的措辭是指發(fā)生動態(tài)綁定的上下文，例如 ref。Reset（。..），所討論的“子類型”是 ref 在這一點(diǎn)上可以引用的對象的類。潛在的類不一定是完整的層次結(jié)構(gòu)，不同的類集可能適用于同一操作的不同調(diào)用。

圖2：與驗證本地類型一致性相關(guān)的活動，DO-332 要求級別為 A、B 或 C 級軟件

考慮引用的特定出現(xiàn)。Reset（。..），并讓 HeatSensor 成為 ref 可以在那里引用的對象可能的子類之一。引用的本地類型一致性。HeatSensor的重置（。..）可以“樂觀地”或“悲觀地”地證明。如果HeatSensor滿足LSP，則樂觀方法有效，可以通過兩種方式進(jìn)行：

通過形式化方法，通過證明HeatSensor的復(fù)位版本滿足傳感器版本的要求，并且不會加強(qiáng)傳感器復(fù)位的前置條件或削弱后置條件。

通過測試，通過使用 HeatSensor 的實(shí)例對傳感器的重置版本運(yùn)行基于要求的測試。

來自編程語言及其工具集（例如 Ada 2012 或 SPARK）的適當(dāng)支持可以促進(jìn)形式化方法。

樂觀的方法將證明超類和子類的操作版本之間的契約和行為一致性。通過對子類的基于需求的測試以及可能通過形式化方法獲得額外的驗證。

如果類不符合 LSP，或者動態(tài)綁定調(diào)用很少，或者層次結(jié)構(gòu)很淺和/或很窄，那么測試可能出現(xiàn)的每種可能的情況可能是最簡單的。這是圖 2 中第三個項目符號項中指定的悲觀測試。需要基于需求的測試來對可能出現(xiàn)的每個子類執(zhí)行操作。

DO-332、本地類型一致性和 LSP 指南認(rèn)證

本地類型一致性驗證只是安全使用 OOT 的一個方面;DO-332 包含有關(guān)其他 OOT 元素以及相關(guān)技術(shù)（如通用模板）的指南。DO-332 是“語言不可知論者”;有關(guān)如何使用 Ada 2012 作為編程語言在安全關(guān)鍵或高安全性系統(tǒng)中應(yīng)用 OOT 的更多細(xì)節(jié)［6］。

DO-332 的本地類型一致性指南與 DO-178C 的一般驗證方法一致，確保所有測試都基于要求。它以一種新穎的方式調(diào)整驗證活動，以反映面向?qū)ο蟮恼Z義和類結(jié)構(gòu)對LSP的遵守程度。新指南應(yīng)有助于促進(jìn)面向?qū)ο缶幊蹋∣OP）在航空電子設(shè)備和其他關(guān)鍵領(lǐng)域的安全使用。

審核編輯：郭婷