汽車電子控制系統安全設計的形式化驗證

摘 要：汽車電子控制系統已成為現代汽車的核心組成部分，因此，深入研究汽車電子控制系統安全設計和驗證方法有助于提高車輛安全性能，增強車輛競爭力。本文闡述了汽車電子控制系統安全性的重要性，探討了當前汽車電子控制系統安全設計和驗證方法的局限性，以及汽車電子控制系統安全設計的形式化驗證方法，形式化驗證方法能夠有效地在產品設計早期識別和消除潛在的問題和安全隱患，為汽車電子控制系統的安全設計和驗證提供了新的思路。

關鍵詞：汽車電子控制系統 安全設計 形式化驗證方法

隨著汽車電子化和智能化程度的不斷提高，汽車電子控制系統在現代汽車中扮演著越來越重要的角色。傳統的汽車電子控制系統安全設計和驗證方法主要依賴于經驗積累和大量的測試，難以全面覆蓋所有可能的故障情況，無法有效應對日益復雜的安全威脅。在此背景下，形式化驗證方法應運而生，它通過嚴格的數學模型和邏輯推理，從系統整體的安全屬性和約束等宏觀角度出發，可以系統地分析和驗證系統的安全性，有助于在設計階段就發現并消除潛在的設計缺陷和安全隱患。

1 汽車電子控制系統安全性的重要性

汽車電子控制系統的安全性對于保障車輛操作的可靠性和乘員的安全至關重要。隨著汽車技術的發展，尤其是在自動駕駛和智能化功能日益增多的當下，汽車電子控制系統扮演了核心角色，其安全性的重要性日益凸顯。

汽車電子控制系統的安全性直接關系到車輛行駛的穩定性和可靠性，這些系統涉及從發動機管理、制動系統到先進的駕駛輔助系統如自動緊急制動（AEB）乃至自動駕駛系統等多個方面。如果汽車電子控制系統存在缺陷或故障，會導致無法預測的車輛危險行為，如意外加速、誤制動或者在緊急情況下無法正確做出反應，從而極大地增加發生事故的風險。因此，汽車電子控制系統的安全性，需要通過嚴謹的安全設計和嚴格的系統驗證來實現，以確保系統在各種行駛條件下均可以穩定、可靠、安全地工作。

2 當前汽車電子控制系統安全設計與驗證面臨的挑戰

盡管汽車制造商和研究機構不斷努力提高電子控制系統的可靠性和安全性，但面對越來越復雜的應用場景和設計，當前的安全設計和驗證方法仍存在一些局限性，這些局限性逐漸成為進一步提升系統的可靠性和穩定性，消除潛在的安全隱患的瓶頸。

2.1 基于場景測試和里程測試的驗證方法

基于場景測試和里程測試的驗證方法都是通過給系統輸入測試樣本數據（基于場景的測試更多的是指定場景作為測試樣本，而基于里程的測試則是隨機樣本），觀測輸出來確認測試結果，并以樣本測試結果通過概率統計方式來評價系統整體設計狀態，這類基于樣本的測試是從一種微觀視角出發來評價系統整體狀態的驗證方法，在覆蓋系統所有可能發生的情況方面存在一定的局限性，尤其是一些極端情況。且測試的質量依賴測試工作人員對系統需求、功能定義、內部外部交互關系等細節的準確理解，這樣才能有效分析關鍵測試點并設計具有重要代表性的測試用例，從而提升對系統整體設計狀態評價的準確性。現代汽車依賴數以百計的電子控制單元（ECU）來管理從發動機運行到自動駕駛的各種功能，在智慧交通高速發展的大背景下，這些功能需要應對越來越多樣化的復雜駕駛場景，同時車輛的外部交互需求（V2X）也不斷提升，系統功能和設計的復雜度與日俱增。系統復雜度的不斷提升給設計工作人員準確表達系統需求和設計，以及測試工作人員充分理解系統需求和設計，分析關鍵測試點并設計高質量測試用例來充分驗證系統滿足安全約束帶來的困難。

而隨著基于機器學習的人工智能技術在汽車電子系統，尤其是自動駕駛系統中越來越廣泛的應用，技術的迭代模式轉為由數據驅動，迭代速度已不可同日而語。

自動駕駛系統已經從以往集中在駕駛輔助SAE Level 1， Level 2功能的水平向更接近自動駕駛的SAE Level 3， Level 4功能進發，這個過程中自動駕駛系統將承擔越來越多的安全職責，對系統安全性的要求越來越苛刻。

汽車電子控制系統驗證的不足會造成潛在缺陷和安全風險在產品上市后才被發現，給用戶安全帶來威脅，系統功能和設計復雜度的提升、技術迭代速度的提升、系統安全性要求的提升這三大因素互相影響，給基于場景測試和里程測試的驗證方法帶來了諸如場景多樣性以及極端場景的稀缺性影響驗證覆蓋度和可實現性、仿真場景和真實場景的差異性對仿真測試結果可信度的影響、高昂的測試成本（時間，人力，財力等多方面成本）等考驗[1]。行業很多研究致力于提升基于場景測試和里程測試的驗證覆蓋度和效率[2]。單純依賴場景測試和里程測試的驗證方法在系統驗證的充分性和完整性方面，尤其針對自動駕駛系統，仍然存在一定的局限性。行業也在不斷探索組合各種不同的驗證方法來提升復雜安全系統驗證的充分性和完整性。

2.2 設計過程中的可驗證

隨著系統復雜度、技術迭代速度、系統安全性要求的不斷提升，對系統開發和驗證的周期以及成本帶來了更大的壓力，我們更希望在產品開發過程中能盡早發現設計中的安全缺陷和不足，越早發現問題，解決問題的時間和經濟成本越低。傳統的針對設計方案驗證方法有：設計評審和安全設計分析，設計評審過程中，評審人員更多憑借經驗教訓，結合一些設計最佳實踐規則來發現方案中的問題點，而安全分析借助一些分析方法如失效模式與影響分析（FMEA），故障樹分析（FTA），數據流和程序流分析結合經驗以及對系統的理解，確認設計方案的正確性和完整性，設計評審和安全設計分析都高度依賴系統需求和設計所展現的信息，參與人員對系統需求和設計的充分理解以及設計經驗，在面對高度復雜的系統時同樣有一定局限性。

3 形式化驗證方法

在汽車電子控制系統日益復雜的背景下，基于場景和里程測試，評審以及安全設計分析的驗證方法在不同程度上展現出一定的局限性。形式化驗證方法作為一種嚴格縝密的系統設計驗證方法，為破局提供了一種新的思路。形式化驗證方法能夠在系統需求定義和設計階段就識別和消除潛在的問題點，顯著提高系統的可靠性和安全性，這種方法通過嚴格的數學和邏輯推理，可以全面分析系統設計模型，驗證其是否滿足預定的安全屬性（也可以稱為安全約束）。形式化驗證方法理論上可以覆蓋系統設計模型完整的狀態空間和行為，相比較基于樣本測試得到的概率統計結論以及高度依賴經驗的設計評審和安全設計分析結果，能夠提供更高的保證級別（Statement Reliability），尤其是處理復雜系統和關鍵安全屬性。優勢主要體現在以下幾個方面：

（1）通過形式化語言（數學和邏輯的語言）能更精確表達需要滿足的安全特性（安全約束），在信息表達的準確度，避免歧義和語義模糊方面明顯優于自然語言，同時通過形式化表達的安全特性（安全約束）是能夠被計算機所理解，能直接作為形式化驗證的依據，方便實現自動化驗證過程。

（2）可以在系統需求定義和設計階段就發現缺陷和不足，有利于降低問題修復成本，提升效率。

（3）鑒于形式化驗證方法理論上可以覆蓋系統設計模型所有可能的狀態和行為，比依賴經驗的設計評審和安全分析，更有利于全面發現設計缺陷。

（4）利用形式化驗證方法，可以幫助驗證測試場景模型與安全特性（安全約束）的匹配程度，提升測試場景覆蓋度，尤其是極端場景。

本文將探討汽車電子控制系統安全設計的形式化驗證方法，闡述其核心組成部分和工作流程。

3.1 形式化規約和建模

在汽車電子控制系統的安全設計中，形式化驗證是一種重要的方法，依賴數學和邏輯上的精確描述來證明形式化規約（Formal Specification）和系統設計模型之間的匹配程度，從而驗證系統設計是否符合預期的安全特性（安全約束）。形式化驗證的過程如圖1，涉及兩個核心步驟：定義形式化規約和構建系統設計的形式化模型。

首先，定義形式化規約，形式化規約是系統需求（包括安全特性）以數學和邏輯表述方式的形式化表達，用以描述系統被期望滿足的時序特性，狀態遷移，功能行為，約束（包含安全約束）等方面的設計要求。而形式化語言是以數學和邏輯表述方式定義形式化規約的重要工具，例如，使用線性時態邏輯（LTL）或信號時態邏輯（STL）來表達系統時序特性，狀態遷移，功能行為，約束（包含安全約束）等方面的設計要求。在形式化語言的幫助下，系統需要滿足的設計要求被全面且精確地描述并形成形式化規約，規約可以被計算機所識別并成為后續形式化驗證的檢驗標準。形式化規約的制定需基于對系統需求的全面理解，包含系統需要遵守功能規范，法規，安全約束，時間和性能限制，異常或者邊界情況下的系統行為等各個方面。

其次，構建系統設計的形式化模型，這一過程中需要將系統的行為、組件和內外部接口、狀態以及時序邏輯這些系統設計細節用形式化建模語言加以描述。例如，設計人員可以使用Petri網來輔助建模[3]，Petri模型能夠描述系統的并發、同步、序列化等過程，不同輸入條件下狀態遷移行為以及時間約束。對于復雜的控制邏輯也可以采用其他建模語言如Alloy或Z語言來表達。系統設計的形式化模型不僅需要能夠精確地反映系統的行為和結構，狀態空間，時序邏輯等方面的設計細節，還應該包含系統可能面臨的各種異常處理和邊界條件，如輸入錯誤、資源不足、輸入處于上下邊界、系統資源臨近限制值，系統響應時間達到或超過時間限制等情況下系統的行為。

通過上述定義形式化規約和構建系統設計的形式化模型這兩個步驟，為后續針對汽車電子控制系統安全設計的形式化驗證做好準備。

3.2 形式化驗證

形式化驗證方法是一種基于數學和邏輯推理及分析來證明系統設計模型滿足形式化規約的方法。常用的形式化驗證方法包含模型檢驗（Model Checking），等效性檢驗（Equivalence checking），理論證明（theorem proving）等[4]。這里主要介紹模型檢驗，模型檢驗通過遍歷系統設計模型所有可能的行為和狀態，檢查是否存在違反形式化規約的情況，主要包含兩部分工作：模型正確性檢驗和模型一致性檢驗。模型正確性檢驗的主要目的確保系統設計模型本身不存在缺陷，依賴一些模型分析工具如Tina（和Petri適配性較好）、Simulink Design Verifier（適用于MATLAB Simulink模型）可以檢查模型并幫助發現諸如邏輯無法被執行（死邏輯）、數組訪問越界和整數溢出、數值超范圍或有效性錯誤、除零等模型設計錯誤。

而模型的一致性檢驗主要的目的是驗證模型與形式化規約的一致性（符合程度），不同于基于樣本的測試從微觀視角出發來評價整體設計狀態的方式，形式化驗證中，測試人員從形式化規約中提取模型的待證明特性（待證明特性可以是系統設計模型期望的輸出結果或者輸出結果的范圍限制來驗證模型的輸出，也可以是包含前置條件（Pre-condition）和后置條件（Post-Condition）的邏輯表達式來驗證模型的行為邏輯，或者其他期望達成的設計結果），通過遍歷系統設計模型所有可能的行為和狀態來尋找待證明特性的反例，如果無法找到反例，則待證明特性成立，系統設計模型滿足對應的形式化規約。這種驗證方法從宏觀視角出發，可以覆蓋模型所有可能的情況，提供更高的保證級別（Statement Reliability），同時模型檢驗的另一個優勢是其能夠提供自動化且全面準確的驗證結果，大大減少人工介入的需求和相關的錯誤可能性。

反例分析是基于模型檢驗的形式化驗證過程中的一個關鍵環節，當模型檢查工具發現待證明特性不成立，它會指出對應的反例，即導致規約違反的具體事件，常見的反例有驗證過程中發現特定情況下系統的輸出與待證明特性不符或超過待證明特性指定的限制范圍，或者在未滿足前置條件（尤其安全相關的條件）的情況下系統就執行了對應動作，又或者前置條件滿足（比如檢測到安全故障）的情況下系統沒有正確執行對應動作（比如關閉執行器并且給駕駛員警告）、執行延遲或超時等等。反例分析的主要任務是分析這些事件的路徑，確定導致待證明特性不成立的原因，并提供有關如何修改設計以解決這些問題的方案，這一過程對于開發者深入理解問題產生的具體場景和原因非常重要。在進行反例分析時，設計人員需要詳細檢查反例提供的信息，包括違反規約的具體狀態轉換、相關變量的值以及觸發錯誤的操作序列。通過這一分析，設計人員可以識別出設計中的問題，問題背后的設計錯誤或者性能瓶頸，并據此調整系統設計，反例的詳細分析還可以幫助改進系統的測試策略，通過針對性地測試那些在模型驗證中已識別為薄弱環節的部分，確保系統的整體穩定性和可靠性。

4 結束語

本文通過探討汽車電子控制系統安全設計的形式化驗證方法，為提高汽車電子系統的安全性和可靠性提供了新的思路。形式化驗證方法能夠有效地在產品設計早期識別和消除系統設計中潛在的問題和安全隱患，提高系統設計的效率和準確性。然而，形式化驗證方法的應用仍面臨著模型復雜度控制、驗證效率提升等挑戰，未來的研究方向應著重于優化形式化模型，提高驗證算法效率，以及探索形式化驗證與其他先進技術如人工智能的融合應用，為汽車產業的健康發展和用戶安全保駕護航。

參考文獻：

[1] W. Ding， C. Xu， M. Arief， H. Lin， B. Li， and D. Zhao， “A survey on safety-critical scenario generation for autonomous driving – a methodological perspective，” 2023.

[2] C. Amersbach and H. Winner， “Defining required and feasible test coverage for scenario-based validation of highly automated vehicles，” in 2019 IEEE Intelligent Transportation Systems Conference （ITSC）， pp. 425–430， IEEE， 2019.

[3]龐明寶，劉震.基于Petri網立交橋智能網聯車協作控制仿真[J].系統仿真學報，2023，35（3）：484-493.

[4]李永明.可能LTL模型檢測的兩種方法[J].陜西師范大學學報（自然科學版），2014（06）：21-25.