英偉達推動(dòng) Ada 和 SPARK 進(jìn)入無(wú)人駕駛汽車(chē)

AdaCore 和 Nvidia 已經(jīng)為 Ada 和 SPARK 編程語(yǔ)言開(kāi)發(fā)了一個(gè)開(kāi)源參考流程，用于安全關(guān)鍵汽車(chē)軟件，特別是自動(dòng)駕駛汽車(chē)。

該流程能夠在 Nvidia DriveOS 操作系統上更快地開(kāi)發(fā) ISO26262 軟件。Nvidia 使用 SPARK 開(kāi)發(fā)了 DriveOS，并為其 DRIVE AGX 硬件上的應用程序開(kāi)發(fā)了認證流程。

基于 Ampere GPU 架構和 ARM Cortex A78AE 內核的 AGX-Orin 芯片，正被包括沃爾沃、梅賽德斯-奔馳、捷豹路虎、通用汽車(chē)、極氪和吉利以及現在豐田（世界上最大的汽車(chē)制造商）等汽車(chē)制造商使用。

基于 Blackwell 架構、搭載 NeoverseV3AE 核心的 AGX-Thor 芯片，預計今年晚些時(shí)候開(kāi)始用于自動(dòng)駕駛。中國電動(dòng)汽車(chē)制造商比亞迪、自動(dòng)駕駛巴士制造商 WeRide、沃爾沃、 卡車(chē)制造商 Aurora、大陸集團和理想汽車(chē)都在使用這款芯片。

DriveOS 芯片在 1 月份通過(guò)了 TUD SUD 的 ASIL-D 認證，采用了名為 Halos 的 AI 安全框架。

“自動(dòng)駕駛的時(shí)代已經(jīng)到來(lái)，我們將與人工智能在制造、企業(yè)以及汽車(chē)模擬和設計方面合作，”英偉達 CEO 黃仁勛表示?！拔覀円呀?jīng)從事自動(dòng)駕駛汽車(chē)研究超過(guò)十年了?！?/p>

參考流程是向前邁進(jìn)的關(guān)鍵一步，包括符合汽車(chē)認證標準 ISO-26262 最高完整性級別的軟件組件。使用 SPARK 需要建立一種開(kāi)發(fā)流程，該流程利用 Ada 形式語(yǔ)言的正式方法和其 SPARK 子集的其他安全特性。

AdaCore 和 Nvidia 決定將參考流程作為一個(gè)開(kāi)放且不斷發(fā)展的文檔發(fā)布，使整個(gè)行業(yè)能夠采用 Ada 和 SPARK。

“這對從事軟件定義汽車(chē)開(kāi)發(fā)的開(kāi)發(fā)者來(lái)說(shuō)是一個(gè)重要的轉折點(diǎn)，”AdaCore 首席產(chǎn)品與營(yíng)收官 Quentin Ochem 告訴 eeNews Europe。

“獨特之處在于 Nvidia 的方法。通過(guò)采用 Ada 和 SPARK 并公開(kāi)發(fā)布其 ISO 26262 合規性文檔，他們正在重塑這些責任的處理方式。Nvidia 沒(méi)有讓開(kāi)發(fā)者負擔隔離的、抽象的合規活動(dòng)，而是將這些考慮因素盡可能接近開(kāi)發(fā)者的主要工件：代碼本身。這符合將驗證、可追溯性和需求直接集成到開(kāi)發(fā)流程中的趨勢，使正確性成為代碼庫的特性，而不僅僅是單獨的過(guò)程?！?/p>

“傳統上，開(kāi)發(fā)者不得不身兼數職——除了編寫(xiě)代碼，他們還常常發(fā)現自己承擔了 QA 工程師、驗證工程師甚至需求工程師的責任，”他補充道。

“像汽車(chē)這樣的安全關(guān)鍵領(lǐng)域，受 ISO 26262 等標準的管轄，需要嚴格的可追溯性、正確性的證據和形式化保證——這些責任遠遠超出了傳統軟件工程的范圍?！?/p>

他還指出，英偉達決定開(kāi)源認證工件是一個(gè)關(guān)鍵舉措。

“也很少見(jiàn)看到主要技術(shù)提供者如此程度地開(kāi)放其內部安全認證流程。英偉達的 ISO 26262 文檔可以即用型使用，這是一個(gè)大事——它為其他汽車(chē)軟件團隊提供了一個(gè)具體、實(shí)用的起點(diǎn)。它降低了開(kāi)發(fā)者和公司構建安全認證車(chē)輛軟件的門(mén)檻，而無(wú)需重新發(fā)明輪子?！?/p>

ISO-26262 參考流程可在 nvidia.github.io/spark-process/ 上獲得，并且任何人都可以自由使用或定制這些語(yǔ)言。

ISO26262 流程

本文檔定義了一個(gè)基于 SPARK 的、符合 ISO-26262 標準的流程，用于開(kāi)發(fā)安全關(guān)鍵車(chē)輛軟件單元的子集，達到 ASIL D 級，并降低 ASIL 等級。

該流程專(zhuān)門(mén)適用于完全使用 Ada 編程語(yǔ)言開(kāi)發(fā)的軟件單元，但面向的是部分或全部 Ada 代碼符合 SPARK 子集的軟件單元。雖然該流程的一些元素，例如所需的 Ada 編譯器警告設置，可能適用于一般的安全關(guān)鍵 Ada 軟件開(kāi)發(fā)，但混合使用 Ada 與其他語(yǔ)言（如 C、C++或匯編語(yǔ)言）的軟件單元不能使用該流程進(jìn)行開(kāi)發(fā)。

該流程涵蓋了與語(yǔ)言子集、軟件單元設計、軟件單元實(shí)現以及軟件單元驗證相關(guān)的 ISO 26262 要求和目標。此外，該流程還涵蓋了與軟件接口規范中表達的安全要求相關(guān)的 ISO 26262 要求和目標。

這個(gè)過(guò)程支持并行進(jìn)行形式化驗證和非形式化驗證。根據此過(guò)程開(kāi)發(fā)的單個(gè)軟件單元可以全部進(jìn)行形式化驗證，全部進(jìn)行非形式化驗證，或者部分進(jìn)行形式化驗證和部分進(jìn)行非形式化驗證。

“簡(jiǎn)而言之，這一舉措有助于消除開(kāi)發(fā)者對安全認證的神秘感，并為更健壯和高效的軟件定義車(chē)輛架構鋪平道路，”Ochem 說(shuō)。

采用一種新的編程語(yǔ)言涉及部署新環(huán)境、培訓團隊適應新的形式化規范、調整編程模式以及其他許多問(wèn)題。然而，從流程的角度來(lái)看，編程語(yǔ)言在很大程度上是可以互換的，但 Ada 和 SPARK 則是一個(gè)不同的故事。

將其視為一種語(yǔ)言轉變是一種可能性，這無(wú)疑會(huì )在傳統的開(kāi)發(fā)過(guò)程中產(chǎn)生價(jià)值。然而，這會(huì )錯失該技術(shù)帶來(lái)的關(guān)鍵機會(huì )，即能夠將開(kāi)發(fā)過(guò)程轉變?yōu)橐则炞C驅動(dòng)的過(guò)程，從而以比傳統方法更嚴格和更具成本效益的方式展示軟件特性。

Ada 語(yǔ)義旨在最小化漏洞風(fēng)險，并最大化直接定義在源代碼中的語(yǔ)義信息。SPARK 使用這些屬性來(lái)避免常見(jiàn)漏洞，并允許定義附加屬性以替代動(dòng)態(tài)測試進(jìn)行形式化驗證。

在 SPARK 中，可以保證變量初始化、無(wú)緩沖區溢出、數據范圍等基本屬性，或者更一般地說(shuō)，避免出現防御性代碼，但它也提供了定義更高級要求的方法，這些要求可以以布爾斷言的形式表達，并且可以正式證明實(shí)現是正確的，而無(wú)需運行任何測試。

以形式化驗證為目標的代碼開(kāi)發(fā)對開(kāi)發(fā)過(guò)程中的各個(gè)層面都有影響。以這種方式開(kāi)發(fā)軟件可能是一個(gè)漫長(cháng)的迭代過(guò)程，存在遺漏技術(shù)某些關(guān)鍵方面的風(fēng)險。

參考流程旨在允許新采用者跳過(guò)這一點(diǎn)，并從已經(jīng)過(guò)當局審查和行業(yè)實(shí)驗的既定流程開(kāi)始。它不是用來(lái)“照搬不照”，而是作為適合每個(gè)組織具體情況的定制流程的起點(diǎn)。

然而 Nvidia 指出，該流程不包括軟件架構設計規范，如何將現有的 C/C++軟件單元移植到基于 SPARK 的流程中，或并發(fā)性或軟件安全分析。