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

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

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

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

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

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

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

繼承和利斯科夫替代原則

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

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

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

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

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

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

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

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

本地類型一致性

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

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

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

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

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

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

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

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

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

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

審核編輯：郭婷