英偉達推動 Ada 和 SPARK 進入無人駕駛汽車

AdaCore 和 Nvidia 已經(jīng)為 Ada 和 SPARK 編程語言開發(fā)了一個開源參考流程，用于安全關鍵汽車軟件，特別是自動駕駛汽車。

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

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

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

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

“自動駕駛的時代已經(jīng)到來，我們將與人工智能在制造、企業(yè)以及汽車模擬和設計方面合作，”英偉達 CEO 黃仁勛表示。“我們已經(jīng)從事自動駕駛汽車研究超過十年了。”

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

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

“這對從事軟件定義汽車開發(fā)的開發(fā)者來說是一個重要的轉折點，”AdaCore 首席產(chǎn)品與營收官 Quentin Ochem 告訴 eeNews Europe。

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

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

“像汽車這樣的安全關鍵領域，受 ISO 26262 等標準的管轄，需要嚴格的可追溯性、正確性的證據(jù)和形式化保證——這些責任遠遠超出了傳統(tǒng)軟件工程的范圍。”

他還指出，英偉達決定開源認證工件是一個關鍵舉措。

“也很少見看到主要技術提供者如此程度地開放其內部安全認證流程。英偉達的 ISO 26262 文檔可以即用型使用，這是一個大事——它為其他汽車軟件團隊提供了一個具體、實用的起點。它降低了開發(fā)者和公司構建安全認證車輛軟件的門檻，而無需重新發(fā)明輪子。”

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

ISO26262 流程

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

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

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

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

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

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

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

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

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

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

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

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