關于自動駕駛車安全保證、驗證和認證的綜述

作者：黃浴 2022-02-21 17:41:32

自動駕駛相關的挑戰不再僅僅集中在自動駕駛車（AV）的制造上，而是在確保其運行安全方面。

arXiv上傳于2022年2月6號的綜述論文“Automated Vehicle Safety Guarantee, Verification and Certification: A Survey”，作者來自美國俄亥俄州立大學。

自動駕駛相關的挑戰不再僅僅集中在自動駕駛車（AV）的制造上，而是在確保其運行安全方面。L3級和L4級自主駕駛的最新進展促使人們對復雜AV機動的安全保證進行了更廣泛的研究，這與ISO21448（即預期功能安全，或SOTIF）的目標一致，即最大限度地減少已知和未知的不安全場景，以及“ 零死亡（VZ） ”——到2050年消除公路死亡事故。

為AV運動控制提供安全保障的大多數方法源自形式（formal）方法，特別是可達性分析（reachability analysis，RA），它依賴于系統動態演化的數學模型來提供保障。該論文綜述了安全檢驗及確認（safety verification & validation）和認證過程（certification process），并回顧了最適合AV的形式（formal）安全技術。

作者提出了一個統一的場景覆蓋框架，可以為全自動駕駛車提供形式（formal）或基于樣本（sample）的安全驗證評估。最后，是AV安全保證的挑戰和未來機會。

此前關于自動駕駛車技術的綜述，一直側重于技術挑戰和實施的各個方面，如感知、決策、車輛控制、人機交互的執行方式，還有一些調查涉及自動駕駛車安全驗證和確認（V&V）問題。

隨著自動駕駛系統在真實世界的部署，針對真實世界中場景的規模，需要進行大量的驗證和確認。最大化場景覆蓋率的常見驗證和確認策略，是在虛擬仿真中驗證，并模擬大量生成的場景樣本。

基于場景采樣的V&V，其面臨的挑戰是，量化能保證合理覆蓋所需的樣本量，從而約束自動駕駛不當驅動造成的風險。合理的場景覆蓋保證也是最近在高度自動駕駛車（HAV）部署的立法中認證的先決條件。然而，另一組基于形式驗證（formal verification）的方法通過規范滿意度（ specification satisfaction）以不同的方法解決場景覆蓋問題。由于形式（formal）方法在場景覆蓋方面的潛力，新興研究已經開始將形式屬性（formal properties）與控制合成（control synthesis）和安全驗證（safety verification）相結合。

鑒于對自動駕駛量化驗證的需求，這里提出一個統一的場景覆蓋框架，來解決自動駕駛場景覆蓋未解決的難點。給定單個場景（基于樣本的方法）的可接受覆蓋表示量，或形式（formal）安全規范的所謂“ 規范穿透率（specification penetration rate） ”，該框架給出統一安全場景覆蓋率的定量定義。該定量定義將基于樣本的方法和形式（formal）方法結合在一起，為安全驗證提供場景覆蓋。候選自動駕駛車控制策略可以通過形式的（formal）或基于樣本的安全驗證，在指定 ODD（operation defined domain）場景測試其安全場景覆蓋率。作者比較基于樣本的方法和形式（formal）方法的優缺點，基于如何達到這種安全覆蓋率，以及方法的相關成本和爭論。

下表是自動駕駛立法的現狀：

責任確定（liability determination）是自動駕駛系統部署需要解決的一個新問題。在L3級，只要意外或困難情況提前移交給駕駛員，自動駕駛系統不承擔責任，因為它只需在其有限的ODD環境中保證安全。即使人類駕駛員沒有及時接管，在一定程度上，諸如制動、停車和打開危險燈等故障安全操作也可以免除自動駕駛系統的責任。當L4級或在其以上的自動駕駛車配備形式安全驗證時，可根據形式邏輯（formal logic）簡化責任確定，如下圖所示：基于樣本的安全驗證開發的自動駕駛系統，目前尚不清楚如何類似的程序執行形式責任確定。

廣泛使用的安全指南標準ISO 26262道路車輛-功能安全，僅適用于緩解與已知部件故障（即已知不安全情況）相關的已知不合理風險，但并未解決復雜環境變量導致的自動駕駛駕駛風險，以及自動駕駛系統如何應對這些風險，而這時候車上沒有任何技術故障發生。

鑒于上述安全挑戰，ISO 21448提出了一個定性目標，該目標描述將自動駕駛功能設計的已知和未知不安全場景結果最小化的目標（goals），如圖所示：

然而，實現這一SOTIF目標的挑戰在于，傳統方法如現場操作測試（field operational test），難以涵蓋測試期間自動駕駛的所有可能場景。盡管存在挑戰，但在安全分析方面仍有一些很有前途的方法和方向，可以朝著ISO 21448的目標前進，例如在模擬測試中最大限度地擴大場景覆蓋率，或通過形式（formal）方法創建安全保證。

在技術術語中，“足夠安全”通常表示指定ODD場景的完整或足夠的場景覆蓋范圍。事實上，現有法規的要求相對較弱，只需要檢查“一些關鍵場景”。

在一個離散場景周圍引入“δ-鄰域”，為場景樣本分配“量”，這是一種很有希望的嘗試。T-wise和泊松過程等數學算法，通過巧妙地選擇樣本有限的候選，可實現 “幾乎全部（almost full） ”的統計覆蓋。

樂觀地假設，這個定量覆蓋-表示問題在整個社區得到了解決和接受，每個采樣場景都有一個“ 覆蓋量（coverage volume） ”。然后，基于樣本方法的完整場景覆蓋任務將執行足夠數量的采樣驗證測試，以確保每個“覆蓋量”單元與至少一個安全測試結果相關聯。

實際上，場景空間的某些存在，恐怕不可能產生安全測試結果（例如，與障礙物的反應距離太小）。這種情況下，需要額外努力來確認這些場景確實不安全。在型式審定和認證方面，當權者需要設定一個可接受的成功門檻，以滿足公眾的期望。最簡單的閾值是，確認安全的不同測試數目與ODD場景測試所需的最小測試數目之比。

多樣化測試場景采樣是在自動駕駛開發階段加強安全控制的主要方法之一。在實現最小化已知和未知不安全場景的SOTIF優化目標方面，基于樣本的方法在發現未知不安全場景方面具有更少的偏差和更多的探索能力，從未知到已知的推動是“水平性“的，即所有采樣場景通常都是在一致的模擬環境和相同的保真度水平。

如圖是形式化方法和基于樣本的方法之間的場景覆蓋率比較：形式化方法從更抽象層的安全規范開始，在場景空間中可能有更大的單一覆蓋量，但將形式化規范集成到控制合成或監控的過程，可能依賴于控制器數學，且繁瑣；由于隨機生成過程，基于樣本的方法的場景覆蓋范圍更分散，但從模擬層開始直接覆蓋案例，這使得采樣過程簡單且易于實現。這兩種方法都試圖將最大限度的驗證場景投射到真實駕駛中，但仿真層和真實駕駛之間的差異始終存在。

與基于測試的安全驗證和保證方法相比，形式（formal）方法具有高的陳述可靠性，因為它有嚴格的邏輯基礎。

自動駕駛車安全中常用的形式（formal）方法包括模型檢查、可達性分析和定理證明。模型檢查起源于軟件開發，以確保軟件行為符合設計規范。當安全規范用公理和引理（axioms & lemmas）表示時，可以用定理證明來驗證最壞情況假設情況下的安全性。可達性分析在這三種分析中占有特殊地位，因為它具有為動態系統生成安全陳述的固有能力，能夠捕捉動態駕駛任務（DDT）的主要特征。

真實世界的道路測試或現場操作測試（FOT）是自動駕駛車驗證和確認（V&V）的最后一步也是昂貴的方法。從某種意義上說，這是唯一的驗證方式。然而，FOT的缺點也很明顯：在車上安裝一個候選自動駕駛控制器情況下，它缺乏足夠的場景覆蓋能力（尤其是接近-碰撞和已經碰撞的場景）。如圖顯示基于樣本、形式（formal）和現場操作測試（FOT）方法的比較：得分為0到10分，10分代表最高滿意度。

形式化（formal）方法是一類應用數學中的嚴格技術（通常以邏輯計算的形式）來實現軟件和工程設計規范和驗證的方法。根據定義，它在安全驗證任務中具有固有的優勢，但具有連續動態的高系統復雜性一直是其在自動駕駛廣泛應用的主要限制因素，即擴展性造成的困難。從技術上講，形式化（formal）方法可以概括為一個實現或者轉換抽象規范為系統控制算法/程序的過程，這樣受控的系統行為可以滿足所述的規范。

定義的動態系統：

最大前向可達集（Maximal Forward Reachable Set）定義如下

前向可達集（FRS）傳播動態，自初始時間t0起，到未來時間t內的所有可能可達狀態。

相反，后向可達集（BRS）的后向傳播，查找來自前一時間t的所有可能狀態，其導致當前時間t0達到某個目標狀態集Xgoal，即如下最大后向可達集（Maximal Backward Reachable Set）的定義

另外，最小BRS定義為：

某些情況下，定義時間范圍內的可達性更令人感興趣。因此，把定義擴展到包括從當前時間到時間范圍結束，比如最大前向可達集的定義修正為（其他類推）：

當不同交通參與者之間的交互起著關鍵作用時，必須將參與有時甚至是對抗智體的影響納入可達性分析。在這種情況下，動態系統要引入額外的輸入d，以表示這種對抗性控制輸入：

這樣的話，系統中對抗性輸入的影響不取決于自車控制，因此必須保守建模，以便在最壞的情況下提供安全保證。

如下是進一步限制在對抗影響下最大FRS的定義：

在計算機科學和機器人技術領域，信號時域邏輯（STL）是一種通用語言，用于表達和指定時間緊要且包含連續變量的需求。如下表列出STL的基本語義。簡言之，STL使用一階邏輯（定義為，一組在非邏輯目標如變量采取量化的形式化系統）對變量的時域發展進行說明。

如下表是基本的STL語義：

自動駕駛車的示例性臨時安全規范可以是“永遠不會在交通中造成碰撞”，但一旦轉換為STL規范，臨時規范中的一些模糊之處需要消除。首先，“原因”一詞在STL中沒有得到很好的定義，因為它涉及碰撞責任認定（liability determination）的復雜性，可能必須用“處于”一詞替換，這是一種責任中立的說法。然后，臨時規范變成了“永遠不要處于交通中的碰撞”。其次，STL要求規范有一個精確定義的時間范圍，對于自動駕駛來說，通常使用時間范圍的概念將時間跨度縮小到一個實用且可處理的水平。因此，臨時規范可以進一步修改為“永不（在時間范圍內）處于沖撞中”。

上述STL翻譯的安全規范在集合語言中仍然停留在抽象層面，自動駕駛車控制算法設計師有責任把規范合成到控制器架構，或對設計的控制器進行安全驗證，有足夠的信心或確鑿的證據確保其滿足規范。

除了控制合成之外，STL表達的安全規范，可以在控制器原型設計期間用作主張，來指明安全違規行為，因此開發人員在控制設計期間要不斷了解安全規范。確定安全規范的邏輯計算，通常通過解決一種決策上的滿足模理論（satisfiability modulo theory，SMT) 問題，來完成。

基于采樣的方法，通過填充大量場景樣本來驗證場景變化。與基于采樣的方法不同，形式化驗證主要是在控制器中實現安全規范，在環境模擬中達到一定的逼真度。這是由于驗證安全的機制不同。在形式化的安全哲學中，安全規范要么得到滿足，要么被違反，把規范的滿足合成到基于模型的控制設計中。這樣設計完成后，在運行過程中確保實現的責任轉移到模型正確性的在線驗證上：只要面向控制的模型驗證為正確的，控制器按照綜合安全規范執行，那么系統就可以證明是安全的。

在不喪失普遍性的情況下，安全規范φ，在某些情況下可能不可行（例如不可避免的碰撞），?u，（s，t ）/|= φ。在這種情況下，φ-綜合控制器，無法找到一個可行的控制序列來實現φ，最好的做法是，將情況提升到有預謀的緊急情況或應變策略（如碰撞沖擊準備）。在任何情況下，由于設計的φ-合成控制器，已經用盡了其可用的動作，仍然無法找到φ-滿足的動作，所以對于不可避免的損壞，控制器不算故障錯誤。

根據ISO 21448，場景（scenario）是一系列情景（scene）中幾個情景之間時域發展的描述，情景是環境的快照，包括景色（scenery）、動態元素、所有參與者和觀察者的自表征，以及這些實體之間的關系。根據這一定義，確保在定義的OOD中完全安全的任務可以描述為，對ODD所有可能場景變化進行安全驗證和確認（V&V）。ODD中場景變化有兩個方面：初始場景的變化，以及自初始場景以來時域發展的變化。場景變化的不同維度如圖所示：

基于樣本的方法并不顯式地擁有與每個樣本場景相關聯的體量屬性，因為每個場景樣本都是基礎的，并且體量較小。為了對兩種安全驗證方法進行統一比較和利用，必須將場景體量（scenario volume）的概念分配給基于樣本的方法。為簡單起見，假設所有N個連續維度彼此正交，并為參數組指定的場景樣本，分配一個N-維場景空間的軸對齊多邊形體量「p01，p02，...，p0N」。

在基于樣本的方法中，在每個場景樣本檢查模擬場景的安全性。另一方面，形式化方法，通常在執行任何仿真之前，先從安全規范開始，然后將規范翻譯成機器可理解的語言聲明，例如線性時域邏輯（LTL）或信號時域邏輯（STL）。然后，應用翻譯的規范，可以通過在模擬/真實世界測試中檢查規范的有效性，或者在控制合成期間將規范轉換為系統約束或其他控制設計功能。

理想情況下，對于形式化方法，如果所有與安全相關的規范首先被真實地轉化為此類機器可理解的陳述，并且如果綜合控制器完全尊重這些陳述，并使用基于模型的控制器對（模擬）環境進行完美建模，那么場景覆蓋率相對于模擬層是100%。

例如，表達式“自動駕駛車輛應始終無碰撞”可以轉換為數學函數形式的可驗證表達式，該數學函數評估自動駕駛車輛與仿真模型中任何其他目標之間的占用重疊，如果仿真中發生重疊，則返回true。

然而，由于以下原因，實際挑戰阻礙了形式化安全規范的100%理想翻譯：首先，形式化方法依賴于基于現實世界抽象的觀點，因此抽象和現實之間的差異（無論大小）將發生，并損害有效的安全保障。第二，實際開發的控制器通常有性能限制，在任何情況下都無法符合安全規范。第三，當形式化安全規范轉換為安全驗證或控制綜合時，存在實際的可擴展性困難。換句話說，形式化方法在現實的滲透率通常低于100%。在形式上，穿透率定義為：形式化安全規范規定的場景子空間中可驗證場景的百分比。

實際上，在指定的ODD中找出自動駕駛車候選控制器的規格滲透率可能是一個挑戰。首先，定理證明等演繹形式化（deductive formal ）方法僅限于相對簡單的離散動態系統，將定理證明擴展到連續動態系統需要進一步建立框架和相當高的計算資源。其次，傳統的算法形式化（algorithmic formal ）方法，如模型檢查，也不適用于連續動態系統，當需要對連續動作空間進行精細離散化時，所有可能動作進行窮舉測試也會產生計算資源問題。然而，將STL與可達性分析相結合的最新進展，可以通過計算ODD場景空間中候選控制器的驗證算術（verification arithmetic）來評估這種穿透率，并預測候選控制器不符合STL規范的體量部分。規范滲透率計算問題仍然是一個開放的問題，未來的工作可能會結合不同的證據收集方法，包括演繹和算法，提供不同的替代方案。

完成場景覆蓋的路線如圖所示：形式化方法和基于樣本的方法都是幫助發現自動駕駛車安全控制弱點的有效工具，自動駕駛車的控制開發者可以根據自己的便利性和偏好選擇其中一種或兩種方法。

該圖實際上是安全驗證的控制政策演變示意圖。在（a）-（e）中，形式化方法從ODD（a）的安全規范開始，然后進行初始安全規范滲透測試，查看安全規范保持得有多好（b）。然后執行可行性檢查，以查看有多少失敗的場景實際上是安全可行的（c）。然后重新設計自動駕駛車的控制器，以修復故障場景量區域（d），最終用候選自動駕駛車控制器驗證所有安全可行場景量的安全性。在（f）-（j）中，基于樣本的方法首先將ODD分割為可驗證的場景單元（f），然后執行不完整的采樣安全測試，檢查候選自動駕駛車控制器（g）的主要問題。隨后進行完全飽和采樣，以確保場景覆蓋率（h）。在全場景覆蓋測試之后，控制器的弱點被暴露出來，重新設計過程將重復（i）。最終，控制器的弱點停止減少，控制器重新設計過程可能結束（j）。請注意，通過形式化方法，可以確定安全不可行的場景區域，并且一旦驗證了ODD中除安全不可行場景體之外的所有體量，就不需要進行進一步重新設計。

安全驗證可以在模擬仿真期間（在線）用預測模塊執行，也可以在模擬仿真之后（離線）執行，簡單地檢查結果，如圖所示即不同驗證方案概覽：

當自車和參與交通智體的控制策略已知（白盒控制）或部分已知（灰色控制）時，形式化方法可以利用這些信息并縮小可達集，提供車輛運動“更緊”的預測，形成在線安全監控和驗證等有價值的應用。相反，如果控制策略是專有的且完全未知（黑盒控制），則安全驗證過程必須涉及每次模擬仿真后黑盒控制器行為的統計學習，這反過來將指導選擇下一個要測試的場景，以更好地針對反例。

A.已知控制政策的形式化安全驗證。如果完全了解控制策略（通常僅限于自車），則可以非常確定地執行安全驗證，有效地消除可達性分析（RA）中的控制變量u。這通常是，計算受控車輛的可達集并將其與相關時間間隔內的障礙物占用集進行比較，來實現的。
B.黑盒控制政策的形式化安全驗證。當控制策略完全未知時，驗證需要退回到不需要控制策略信息的更一般的計劃。此類計劃將控制器和平臺視為一個整體系統，并調查整個系統的輸入（如干擾）如何導致不期望的輸出（如安全違規）。一項關于黑盒驗證的綜述論文列出模擬退火、進化算法、貝葉斯優化或擴展蟻群優化（ant colony optimization）等幾種方法。
C.灰盒控制政策的形式化安全驗證。如果控制策略部分已知，則可以執行修改的可達性分析（RA）形式化方法。在半自動車輛的設置中，人類駕駛員的行為最多只能進行估計，必須用部分已知的控制策略（本例即人類駕駛員策略）進行安全驗證。在此設置中，設計的特定車道保持輔助控制器將人類駕駛員的轉向策略視為已知且不可變，而將人類駕駛員的加速策略視為未知且可變。這種處理方法允許可達性分析（RA）在適當的時間范圍內預測車輛的可達狀態范圍，系統可以通過比較當前車輛狀態和后向可達安全集（BRS）來確定人類駕駛員是否需要幫助。當至少知道控制策略或功能的定性目標時（例如，激活干預，避免車輛因駕駛員誤操作而發生可避免的碰撞），則可以使用可達性分析（RA）來驗證此類控制策略或功能是否忠實于其定性描述。例如，用于判斷防撞系統是否錯過或濫用了干預機會。

如下表是：可達性分析（RA）部署的形式化和提供的保證類型

形式化（formal）方法可以提供有關當前駕駛狀況緊要性的有用信息。該信息可用于制定標準，以確定是否需要不同的控制方案，從安全緊要場景中把自車帶入安全。

其中一個仲裁標準是車輛是否處于不可避免碰撞狀態（inevitable collision state，ICS），有人認為，在估計碰撞頻率時，這是一個比傳統的威脅度量，如碰撞時間（TTC），更可靠的碰撞接近度量，是ISO26262中確定汽車安全完整性水平（automotive safety integritity level，ASIL）的關鍵量。如果車輛確實處于這種狀態，則應進行碰撞準備（通常通過制動減速或遵循非故障軌跡），因為碰撞是不可避免的。該概念已被用于ADAS功能原型，如確定何時觸發自動緊急制動（AEB）或執行避碰動作。為了確定此類ICS，通常使用可達性分析（RA）。當移動障礙物的預測在動態交通場景中至關重要時，創建ICS概率等價的概率框架。對于某些半自動駕駛或ADAS功能，確定系統是否處于不可避免碰撞狀態（ICS）有助于確定ADAS干預是否遺漏或不必要。

另一個仲裁標準是，在系統當前的運動模式下，目標狀態是否可以實現。例如，用修剪軌跡的概念對車輛的運動模式進行分類，其特征是保持運動所需的恒定輸入。可以建立某個系統的軌跡庫，供控制器從中選擇。在這種情況下，持續的可行性（continuous feasibility）和控制活力（control liveliness）是確保完成更高級任務的關鍵因素，如超車、并入繁忙的快車道或避開高速的障礙物。如果從大型復雜動態模式庫中選擇模式需要計算，可以利用基于學習的方法（如強化學習），根據環境有效地學習適當的模式仲裁決策。

可達性也可以“隨時”直接集成到控制系統中，為現任控制器提供持續的指導/傾向性，避免不可能的控制造成的災難性事件。

這種直接控制集成方法之一是模型預測控制（MPC），其中可以使用形式化方法，尤其是可達性分析（RA）來開發魯棒的MPC算法，如圖所示：可達性分析用于為每個MPC規劃范圍找到可行的狀態集，這樣生成的MPC算法不會試圖在不可行區域中找到最優解，因為那些區域會導致不穩定或控制失敗。