Nvidia將Ada和SPARK引入無人駕駛汽車

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

該流程支持在 Nvidia DriveOS作系統之上更快地開發 ISO26262 軟件。Nvidia 使用 SPARK 開發了具有 7m 行代碼的 DriveOS，以及基于其 DRIVE AGX 的硬件上的應用程序的認證流程。

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

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

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

“自動駕駛汽車的時代已經到來，我們將在制造、企業以及它們模擬和設計汽車和汽車的方式中與 AI 合作，”Nvidia 首席執行官黃仁勛表示。“十多年來，我們一直在研究自動駕駛汽車。”

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

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

“這標志著開發人員在軟件定義汽車上工作的一個重要轉折點，”AdaCore的首席產品和收入官Quentin Ochem告訴eeNews Europe。

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

“傳統上，開發人員不得不身兼數職——除了編寫代碼之外，他們經常發現自己承擔了 QA 工程師、驗證工程師甚至需求工程師的責任，”他補充道。

“像汽車這樣的安全關鍵領域受 ISO 26262 等標準的約束，需要嚴格的可追溯性、正確性證據和正式保證——這些責任遠遠超出了傳統的軟件工程。”

他還指出，Nvidia 決定開源認證工件是一項關鍵舉措。

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

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

ISO26262

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

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

此過程涵蓋與語言子集、軟件單元設計、軟件單元實施和軟件單元驗證相關的 ISO 26262 要求和目標。此外，該流程還涵蓋了 ISO 26262 要求和與安全要求相關的目標，當它們以軟件接口規范表達時。

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

“簡而言之，此舉有助于為開發人員揭開安全認證的神秘面紗，并為更強大、更高效的軟件定義汽車架構鋪平道路，”Ochem 說。

采用新的編程語言涉及部署新環境、培訓團隊以適應新的形式、調整編程模式以及許多其他問題。但是，從過程的角度來看，編程語言可以互換，但 Ada 和 SPARK 是另一回事。

將其視為一種語言轉變是一種可能性，這肯定會在傳統的開發過程中產生價值。然而，這將錯過該技術帶來的關鍵機會，即將開發過程轉變為驗證驅動過程的能力，從而允許以比傳統方法更嚴格、更具成本效益的方式演示軟件屬性。

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

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

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

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

然而，Nvidia 指出，該流程并未涵蓋軟件架構設計規范、如何將現有 C/C++ 軟件單元移植到這個基于 Spark 的進程，或者并發或軟件安全分析。