Nvidia將Ada和SPARK引入無(wú)人駕駛汽車(chē)

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

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

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

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

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

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

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

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

“這標志著(zhù)開(kāi)發(fā)人員在軟件定義汽車(chē)上工作的一個(gè)重要轉折點(diǎn)，”AdaCore的首席產(chǎn)品和收入官Quentin Ochem告訴eeNews Europe。

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

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

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

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

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

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

ISO26262

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

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

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

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

“簡(jiǎn)而言之，此舉有助于為開(kāi)發(fā)人員揭開(kāi)安全認證的神秘面紗，并為更強大、更高效的軟件定義汽車(chē)架構鋪平道路，”Ochem 說(shuō)。

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

將其視為一種語(yǔ)言轉變是一種可能性，這肯定會(huì )在傳統的開(kāi)發(fā)過(guò)程中產(chǎn)生價(jià)值。然而，這將錯過(guò)該技術(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)測試。

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

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

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

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