AdaCore 和 Nvidia 為安全關(guān)鍵型汽車軟件中的 Ada 和 SPARK 編程語言開發(fā)了開源參考流程，特別是對于無人駕駛汽車。

該流程支持在 Nvidia DriveOS作系統(tǒng)之上更快地開發(fā) ISO26262 軟件。Nvidia 使用 SPARK 開發(fā)了具有 7m 行代碼的 DriveOS，以及基于其 DRIVE AGX 的硬件上的應(yīng)用程序的認(rèn)證流程。

AGX-Orin 芯片基于 Ampere GPU 架構(gòu)和 ARM Cortex A78AE 內(nèi)核，被沃爾沃、梅賽德斯-奔馳、捷豹路虎、通用汽車、極氪和吉利等汽車制造商以及全球最大的汽車制造商豐田使用。

基于 Blackwell 架構(gòu)、搭載 NeoverseV3AE 內(nèi)核的 AGX-Thor 芯片預(yù)計將于今年晚些時候提供自動駕駛樣品。中國電動汽車制造商比亞迪、自動駕駛班車制造商文遠(yuǎn)知行、沃爾沃、卡車制造商極光、大陸集團(tuán)和理想汽車都在使用。

DriveOS 于 1 月在 Orin 芯片上獲得了 TUD SUD 的 ASIL-D 認(rèn)證，該芯片具有名為 Halos 的 AI 安全框架。

“自動駕駛汽車的時代已經(jīng)到來，我們將在制造、企業(yè)以及它們模擬和設(shè)計汽車和汽車的方式中與 AI 合作，”Nvidia 首席執(zhí)行官黃仁勛表示。“十多年來，我們一直在研究自動駕駛汽車?！?/p>

參考流程是向前邁出的關(guān)鍵一步，包括符合汽車認(rèn)證標(biāo)準(zhǔn) ISO-26262 最高完整性級別的軟件組件。使用 SPARK 需要建立一個開發(fā)流程，該流程利用 Ada 形式語言及其 SPARK 子集的形式化方法和其他安全特性。

AdaCore 和 Nvidia 已決定將參考流程作為開源且不斷發(fā)展的文檔發(fā)布，從而允許整個行業(yè)采用 Ada 和 SPARK。

“這標(biāo)志著開發(fā)人員在軟件定義汽車上工作的一個重要轉(zhuǎn)折點，”AdaCore的首席產(chǎn)品和收入官Q(mào)uentin Ochem告訴eeNews Europe。

“這里的獨特之處在于 Nvidia 的方法。通過采用 Ada 和 SPARK 并公開發(fā)布其 ISO 26262 認(rèn)證文件，他們正在重塑這些職責(zé)的處理方式。Nvidia 沒有讓開發(fā)人員承擔(dān)孤立、抽象的合規(guī)活動，而是將這些問題盡可能地接近開發(fā)人員的主要工件：代碼本身。這與將驗證、可追溯性和需求直接集成到開發(fā)流程中的增長趨勢相一致，使正確性成為代碼庫的一個屬性，而不僅僅是一個單獨的過程。

“傳統(tǒng)上，開發(fā)人員不得不身兼數(shù)職——除了編寫代碼之外，他們經(jīng)常發(fā)現(xiàn)自己承擔(dān)了 QA 工程師、驗證工程師甚至需求工程師的責(zé)任，”他補(bǔ)充道。

“像汽車這樣的安全關(guān)鍵領(lǐng)域受 ISO 26262 等標(biāo)準(zhǔn)的約束，需要嚴(yán)格的可追溯性、正確性證據(jù)和正式保證——這些責(zé)任遠(yuǎn)遠(yuǎn)超出了傳統(tǒng)的軟件工程。”

他還指出，Nvidia 決定開源認(rèn)證工件是一項關(guān)鍵舉措。

“很少看到主要技術(shù)提供商將其內(nèi)部安全認(rèn)證流程開放到這種程度。Nvidia 的 ISO 26262 文檔可以現(xiàn)成使用，這是一件大事，它為其他汽車軟件團(tuán)隊提供了一個具體、實用的起點。它降低了開發(fā)人員和公司的需求門檻，這些公司的目標(biāo)是構(gòu)建安全、經(jīng)過認(rèn)證的車輛軟件，而無需重新發(fā)明輪子。

ISO-26262 參考流程可在 nvidia.github.io/spark-process/ 上獲得，任何有興趣采用這些語言的人都可以自由使用或定制。

ISO26262

該文件定義了一個基于 Spark 的 ISO-26262 合規(guī)流程，用于開發(fā)符合 ASIL D 和更低 ASIL 的安全關(guān)鍵型車輛軟件單元子集。

該過程僅適用于完全使用 Ada 編程語言開發(fā)的軟件單元，但面向部分或全部 Ada 代碼符合 SPARK 子集的軟件單元。雖然此過程的某些元素（例如所需的 Ada 編譯器警告設(shè)置）通常適用于安全關(guān)鍵型 Ada 軟件開發(fā)，但無法使用此流程開發(fā)將 Ada 與其他語言（例如 C、C++ 或匯編語言）混合的軟件單元。

此過程涵蓋與語言子集、軟件單元設(shè)計、軟件單元實施和軟件單元驗證相關(guān)的 ISO 26262 要求和目標(biāo)。此外，該流程還涵蓋了 ISO 26262 要求和與安全要求相關(guān)的目標(biāo)，當(dāng)它們以軟件接口規(guī)范表達(dá)時。

此過程支持并排進(jìn)行形式驗證和非形式驗證。根據(jù)此流程開發(fā)的單個軟件單元可以進(jìn)行整體正式驗證、整體非正式驗證，或者部分正式驗證和部分非正式驗證。

“簡而言之，此舉有助于為開發(fā)人員揭開安全認(rèn)證的神秘面紗，并為更強(qiáng)大、更高效的軟件定義汽車架構(gòu)鋪平道路，”O(jiān)chem 說。

采用新的編程語言涉及部署新環(huán)境、培訓(xùn)團(tuán)隊以適應(yīng)新的形式、調(diào)整編程模式以及許多其他問題。但是，從過程的角度來看，編程語言可以互換，但 Ada 和 SPARK 是另一回事。

將其視為一種語言轉(zhuǎn)變是一種可能性，這肯定會在傳統(tǒng)的開發(fā)過程中產(chǎn)生價值。然而，這將錯過該技術(shù)帶來的關(guān)鍵機(jī)會，即將開發(fā)過程轉(zhuǎn)變?yōu)轵炞C驅(qū)動過程的能力，從而允許以比傳統(tǒng)方法更嚴(yán)格、更具成本效益的方式演示軟件屬性。

Ada 語義旨在最大限度地降低漏洞風(fēng)險，并最大限度地利用源代碼中直接定義的語義信息。SPARK 使用這些屬性來避免常見漏洞，并允許定義其他屬性以正式驗證以代替動態(tài)測試。

在 SPARK 中，可以保證基本屬性，例如變量初始化、沒有緩沖區(qū)溢出、數(shù)據(jù)范圍，或者更普遍地說，否則最終會成為防御性代碼，但它也提供了定義更高級要求的方法，這些要求可以以布爾斷言的形式表示，并且無需運行測試即可正式證明實現(xiàn)是正確的。

在開發(fā)代碼時考慮形式化驗證會在開發(fā)過程的各個級別產(chǎn)生影響。建立一種以這種方式開發(fā)軟件的方法可能是一個漫長的迭代路徑，并且可能會錯過技術(shù)的某些關(guān)鍵方面。

參考流旨在允許新的采用者跳過此步驟，并啟動一個已經(jīng)建立的流程，該流程已經(jīng)過權(quán)威機(jī)構(gòu)的審查并由行業(yè)進(jìn)行試驗。它并不意味著“按原樣”使用，而是作為適合每個組織具體情況的定制流程的起點。

然而，Nvidia 指出，該流程并未涵蓋軟件架構(gòu)設(shè)計規(guī)范、如何將現(xiàn)有 C/C++ 軟件單元移植到這個基于 Spark 的進(jìn)程，或者并發(fā)或軟件安全分析。