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

該流程支持在 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ù)計(jì)將于今年晚些時(shí)候提供自動(dòng)駕駛樣品。中國(guó)電動(dòng)汽車制造商比亞迪、自動(dòng)駕駛班車制造商文遠(yuǎn)知行、沃爾沃、卡車制造商極光、大陸集團(tuán)和理想汽車都在使用。

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

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

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

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

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

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

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

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

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

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

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

ISO26262

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

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

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

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

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

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

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

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

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

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

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

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