汽車電子控制系統(tǒng)安全設(shè)計(jì)的形式化驗(yàn)證

摘 要：汽車電子控制系統(tǒng)已成為現(xiàn)代汽車的核心組成部分，因此，深入研究汽車電子控制系統(tǒng)安全設(shè)計(jì)和驗(yàn)證方法有助于提高車輛安全性能，增強(qiáng)車輛競(jìng)爭(zhēng)力。本文闡述了汽車電子控制系統(tǒng)安全性的重要性，探討了當(dāng)前汽車電子控制系統(tǒng)安全設(shè)計(jì)和驗(yàn)證方法的局限性，以及汽車電子控制系統(tǒng)安全設(shè)計(jì)的形式化驗(yàn)證方法，形式化驗(yàn)證方法能夠有效地在產(chǎn)品設(shè)計(jì)早期識(shí)別和消除潛在的問(wèn)題和安全隱患，為汽車電子控制系統(tǒng)的安全設(shè)計(jì)和驗(yàn)證提供了新的思路。

關(guān)鍵詞：汽車電子控制系統(tǒng) 安全設(shè)計(jì) 形式化驗(yàn)證方法

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

1 汽車電子控制系統(tǒng)安全性的重要性

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

汽車電子控制系統(tǒng)的安全性直接關(guān)系到車輛行駛的穩(wěn)定性和可靠性，這些系統(tǒng)涉及從發(fā)動(dòng)機(jī)管理、制動(dòng)系統(tǒng)到先進(jìn)的駕駛輔助系統(tǒng)如自動(dòng)緊急制動(dòng)（AEB）乃至自動(dòng)駕駛系統(tǒng)等多個(gè)方面。如果汽車電子控制系統(tǒng)存在缺陷或故障，會(huì)導(dǎo)致無(wú)法預(yù)測(cè)的車輛危險(xiǎn)行為，如意外加速、誤制動(dòng)或者在緊急情況下無(wú)法正確做出反應(yīng)，從而極大地增加發(fā)生事故的風(fēng)險(xiǎn)。因此，汽車電子控制系統(tǒng)的安全性，需要通過(guò)嚴(yán)謹(jǐn)?shù)陌踩O(shè)計(jì)和嚴(yán)格的系統(tǒng)驗(yàn)證來(lái)實(shí)現(xiàn)，以確保系統(tǒng)在各種行駛條件下均可以穩(wěn)定、可靠、安全地工作。

2 當(dāng)前汽車電子控制系統(tǒng)安全設(shè)計(jì)與驗(yàn)證面臨的挑戰(zhàn)

盡管汽車制造商和研究機(jī)構(gòu)不斷努力提高電子控制系統(tǒng)的可靠性和安全性，但面對(duì)越來(lái)越復(fù)雜的應(yīng)用場(chǎng)景和設(shè)計(jì)，當(dāng)前的安全設(shè)計(jì)和驗(yàn)證方法仍存在一些局限性，這些局限性逐漸成為進(jìn)一步提升系統(tǒng)的可靠性和穩(wěn)定性，消除潛在的安全隱患的瓶頸。

2.1 基于場(chǎng)景測(cè)試和里程測(cè)試的驗(yàn)證方法

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

而隨著基于機(jī)器學(xué)習(xí)的人工智能技術(shù)在汽車電子系統(tǒng)，尤其是自動(dòng)駕駛系統(tǒng)中越來(lái)越廣泛的應(yīng)用，技術(shù)的迭代模式轉(zhuǎn)為由數(shù)據(jù)驅(qū)動(dòng)，迭代速度已不可同日而語(yǔ)。

自動(dòng)駕駛系統(tǒng)已經(jīng)從以往集中在駕駛輔助SAE Level 1， Level 2功能的水平向更接近自動(dòng)駕駛的SAE Level 3， Level 4功能進(jìn)發(fā)，這個(gè)過(guò)程中自動(dòng)駕駛系統(tǒng)將承擔(dān)越來(lái)越多的安全職責(zé)，對(duì)系統(tǒng)安全性的要求越來(lái)越苛刻。

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

2.2 設(shè)計(jì)過(guò)程中的可驗(yàn)證

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

3 形式化驗(yàn)證方法

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

（1）通過(guò)形式化語(yǔ)言（數(shù)學(xué)和邏輯的語(yǔ)言）能更精確表達(dá)需要滿足的安全特性（安全約束），在信息表達(dá)的準(zhǔn)確度，避免歧義和語(yǔ)義模糊方面明顯優(yōu)于自然語(yǔ)言，同時(shí)通過(guò)形式化表達(dá)的安全特性（安全約束）是能夠被計(jì)算機(jī)所理解，能直接作為形式化驗(yàn)證的依據(jù)，方便實(shí)現(xiàn)自動(dòng)化驗(yàn)證過(guò)程。

（2）可以在系統(tǒng)需求定義和設(shè)計(jì)階段就發(fā)現(xiàn)缺陷和不足，有利于降低問(wèn)題修復(fù)成本，提升效率。

（3）鑒于形式化驗(yàn)證方法理論上可以覆蓋系統(tǒng)設(shè)計(jì)模型所有可能的狀態(tài)和行為，比依賴經(jīng)驗(yàn)的設(shè)計(jì)評(píng)審和安全分析，更有利于全面發(fā)現(xiàn)設(shè)計(jì)缺陷。

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

本文將探討汽車電子控制系統(tǒng)安全設(shè)計(jì)的形式化驗(yàn)證方法，闡述其核心組成部分和工作流程。

3.1 形式化規(guī)約和建模

在汽車電子控制系統(tǒng)的安全設(shè)計(jì)中，形式化驗(yàn)證是一種重要的方法，依賴數(shù)學(xué)和邏輯上的精確描述來(lái)證明形式化規(guī)約（Formal Specification）和系統(tǒng)設(shè)計(jì)模型之間的匹配程度，從而驗(yàn)證系統(tǒng)設(shè)計(jì)是否符合預(yù)期的安全特性（安全約束）。形式化驗(yàn)證的過(guò)程如圖1，涉及兩個(gè)核心步驟：定義形式化規(guī)約和構(gòu)建系統(tǒng)設(shè)計(jì)的形式化模型。

首先，定義形式化規(guī)約，形式化規(guī)約是系統(tǒng)需求（包括安全特性）以數(shù)學(xué)和邏輯表述方式的形式化表達(dá)，用以描述系統(tǒng)被期望滿足的時(shí)序特性，狀態(tài)遷移，功能行為，約束（包含安全約束）等方面的設(shè)計(jì)要求。而形式化語(yǔ)言是以數(shù)學(xué)和邏輯表述方式定義形式化規(guī)約的重要工具，例如，使用線性時(shí)態(tài)邏輯（LTL）或信號(hào)時(shí)態(tài)邏輯（STL）來(lái)表達(dá)系統(tǒng)時(shí)序特性，狀態(tài)遷移，功能行為，約束（包含安全約束）等方面的設(shè)計(jì)要求。在形式化語(yǔ)言的幫助下，系統(tǒng)需要滿足的設(shè)計(jì)要求被全面且精確地描述并形成形式化規(guī)約，規(guī)約可以被計(jì)算機(jī)所識(shí)別并成為后續(xù)形式化驗(yàn)證的檢驗(yàn)標(biāo)準(zhǔn)。形式化規(guī)約的制定需基于對(duì)系統(tǒng)需求的全面理解，包含系統(tǒng)需要遵守功能規(guī)范，法規(guī)，安全約束，時(shí)間和性能限制，異?；蛘哌吔缜闆r下的系統(tǒng)行為等各個(gè)方面。

其次，構(gòu)建系統(tǒng)設(shè)計(jì)的形式化模型，這一過(guò)程中需要將系統(tǒng)的行為、組件和內(nèi)外部接口、狀態(tài)以及時(shí)序邏輯這些系統(tǒng)設(shè)計(jì)細(xì)節(jié)用形式化建模語(yǔ)言加以描述。例如，設(shè)計(jì)人員可以使用Petri網(wǎng)來(lái)輔助建模[3]，Petri模型能夠描述系統(tǒng)的并發(fā)、同步、序列化等過(guò)程，不同輸入條件下?tīng)顟B(tài)遷移行為以及時(shí)間約束。對(duì)于復(fù)雜的控制邏輯也可以采用其他建模語(yǔ)言如Alloy或Z語(yǔ)言來(lái)表達(dá)。系統(tǒng)設(shè)計(jì)的形式化模型不僅需要能夠精確地反映系統(tǒng)的行為和結(jié)構(gòu)，狀態(tài)空間，時(shí)序邏輯等方面的設(shè)計(jì)細(xì)節(jié)，還應(yīng)該包含系統(tǒng)可能面臨的各種異常處理和邊界條件，如輸入錯(cuò)誤、資源不足、輸入處于上下邊界、系統(tǒng)資源臨近限制值，系統(tǒng)響應(yīng)時(shí)間達(dá)到或超過(guò)時(shí)間限制等情況下系統(tǒng)的行為。

通過(guò)上述定義形式化規(guī)約和構(gòu)建系統(tǒng)設(shè)計(jì)的形式化模型這兩個(gè)步驟，為后續(xù)針對(duì)汽車電子控制系統(tǒng)安全設(shè)計(jì)的形式化驗(yàn)證做好準(zhǔn)備。

3.2 形式化驗(yàn)證

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

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

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

4 結(jié)束語(yǔ)

本文通過(guò)探討汽車電子控制系統(tǒng)安全設(shè)計(jì)的形式化驗(yàn)證方法，為提高汽車電子系統(tǒng)的安全性和可靠性提供了新的思路。形式化驗(yàn)證方法能夠有效地在產(chǎn)品設(shè)計(jì)早期識(shí)別和消除系統(tǒng)設(shè)計(jì)中潛在的問(wèn)題和安全隱患，提高系統(tǒng)設(shè)計(jì)的效率和準(zhǔn)確性。然而，形式化驗(yàn)證方法的應(yīng)用仍面臨著模型復(fù)雜度控制、驗(yàn)證效率提升等挑戰(zhàn)，未來(lái)的研究方向應(yīng)著重于優(yōu)化形式化模型，提高驗(yàn)證算法效率，以及探索形式化驗(yàn)證與其他先進(jìn)技術(shù)如人工智能的融合應(yīng)用，為汽車產(chǎn)業(yè)的健康發(fā)展和用戶安全保駕護(hù)航。

參考文獻(xiàn)：

[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網(wǎng)立交橋智能網(wǎng)聯(lián)車協(xié)作控制仿真[J].系統(tǒng)仿真學(xué)報(bào)，2023，35（3）：484-493.

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