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

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

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

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

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

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

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

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

下表是自動駕駛立法的現(xiàn)狀：

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

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

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

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

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

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

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

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

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

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

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

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

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

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

定義的動態(tài)系統(tǒng)：

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

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

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

另外，最小BRS定義為：

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

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

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

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

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

如下表是基本的STL語義：

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

這也被稱為遞歸可行性或持久可行性。當可達集約束為概率時，可以開發(fā)魯棒MPC隨機等價的模型。除了魯棒性和可行性保證之外，RA應用于MPC的其他好處，包括建立系統(tǒng)輸入到狀態(tài)穩(wěn)定性的潛在方法，將基于學習MPC的魯棒性和性能分離，移除永遠無法到達的區(qū)域來顯式降低MPC的復雜性。

將形式安全性集成到控制設計中的另一種方法是生成安全參考軌跡，如圖所示：可達性可用于軌跡規(guī)劃階段，生成最安全且物理上可行的軌跡，供較低層的控制器遵循。

最后是安全的開放性問題和資源

1 開放性問題

• 1） 保真度-速度權衡
• 2） 數(shù)據(jù)驅(qū)動的可達性方法
• 3） 超越二進制安全驗證
• 4） 構(gòu)建安全描述的新邏輯
• 5） 具有可達性的道德驗證

2 資源問題

1） 可達性分析的數(shù)值方法

如下表所示的清單：

2） 可達性分析的軟件工具

如下表給出的清單：