軌道交通控制軟件中基于場景的需求分析方法

閆倩倩，繆煒愷

（華東師范大學上海市高可信計算重點實驗室，上海 200062）

0 概述

對于軌道交通系統、航空航天控制系統、核電控制系統等安全控制系統，其嵌入式控制軟件是否能正確執行預期功能會影響到人身安全。因此，如何確保嵌入式控制軟件的正確性成為研究人員的關注熱點［1-3］。眾所周知，形式化的需求規約可有效提高軟件的質量，精確描述軟件功能，并通過形式化建模執行嚴格的需求確認和驗證，為后續的開發提供便利。

然而，如何把形式化方法應用到真實的工業軟件中依然是一大挑戰［4］。首先，目前缺乏建立形式化規約的方法。一方面，由于軟件需求大多使用自然語言撰寫而自然語言描述具有不準確性，軟件工程師在構建需求規約時未必能準確且精確地描述系統功能；另一方面，領域專家幾乎不可能使用復雜的形式化表示法描述系統需求，多數領域專家缺少堅實的離散數學基礎，并且學習復雜的數學符號和證明技巧既費時又費力。其次，形式化的需求確認和驗證大多由軟件工程師主導，缺乏領域專家視角。傳統的形式化驗證側重于使用形式化證明方法發現軟件中的邏輯錯誤，如不一致性，但這對領域專家來說是難以理解的。

在形式化方法的需求建模階段，根據不同的建模需求，大致有基于統一建模語言的方法UML［5］、基于屬性描述語言的方法PSL［6］、基于規約描述語言的方法SDL［7］、基于邏輯的方法Z［8］和Event-B［9-10］、基于進程代數的方法CCS［11］和CSP［12］等。而在需求分析階段，需求審查因其易推廣、實施容易的特點，廣泛應用于需求確認過程中。研究人員提出了一系列需求審查方法，如基于查詢模型的提問式審查方法［13］、以認知模型為基礎的審查方法［14］、以虛擬原型為基礎的審查方法［15］等。規約測試技術也是一種經常應用于需求確認的方法。VDMTools 工具［16］執行用VDM 語言寫成的規約顯示系統動作供測試人員確認。同時，ProB 為B 語言需求規約提供一種確認手段［17］。模型檢查也是一種常用的形式化分析方法，如：基于特定語言的建模方法DSL［18-19］；一種用EAST-ADL 描述的架構模型分析技術［20］，包括EAST-ADL 的模擬執行；基于組件的BIP 模型被用來進行軟件建模和驗證［21］，用于對無界時間屬性的馬爾可夫鏈進行統計模型檢查的算法［22］等。在工業上的應用方面，StateChart 廣泛應用于工業軟件建模和分析［23］，Matlab/Simulink 提供了Stateflow［24］。然而這些方法都沒有為大型工業項目提供一個系統的需求建模方法。

場景是一種用于分析軟件的重要途徑，且符合領域專家的思維方式。在基于場景的設計分析方面，基于模型驅動的方式被廣泛使用。基于場景的CBTC（Communication Based Train Control）系統建模［25］方法，通過場景模型和需求間的追溯關系，指導如何撰寫場景的方法［26］，用一階線性邏輯驗證需求場景的正確性等方法［27］。目前，研究人員大都關注軟件代碼功能，生成測試用例，給出優化方法［28-29］。然而這些方法都沒有提供一個基于物理場景的需求確認和驗證方法。

本文針對面向軌道交通領域的嵌入式控制軟件，提出一種以領域專家為中心的基于場景的需求分析方法。使用三步演化式建模方法建立形式化的需求規約，避免復雜的數學運算，并導出需求模型。在此基礎上，領域專家根據規則撰寫場景分析場景執行結果驗證需求規約是否正確地描述了期望的場景。為驗證需求的正確性，提高需求確認和驗證的效率，分別從特殊變量場景、效率、場景質量這3 個方面對場景進行優化。

1 方法框架

如圖1 所示，本文方法主要包括演化式需求建模和需求的確認和驗證2 個部分。首先，通過和領域專家的大量交流，從嵌入式控制軟件中提取特定領域的特征，并根據這些周期性、模式轉化等特征，建立需求規約模板，領域專家可以根據模板的指導使用自然語言構建非形式化規約，軟件工程師和領域專家都可以快速地理解非形式化需求；然后，在非形式化需求被確認后，非形式化需求被轉化為半形式化需求，所有的數據結構都被形式化的定義，在這個階段，系統結構仍然可以被方便的修改重塑；最后，當半形式化規約確認后，用戶需求被最終轉化為形式化地需求規約，此時，所有的變量、功能都被形式化地定義。

圖1 本文方法框架Fig.1 Framework of the proposed method

需求形式化規約構建完成后，接下來驗證需求正確性，需求規約首先被轉化為形式化需求模型。在嵌入式控制軟件領域，傳統的基于場景的測試方法是把場景放到仿真平臺上執行，然而對大規模的嵌入式軟件來說，為了驗證其中一個子系統的需求正確性，仿真執行時需要配置大量初始信息，費時費力。設想，如果場景能直接在需求模型中執行，則可以節約大量時間資源。為此，本文規定場景描述規則，即在場景中加入相關需求變量的取值，從而在執行需求模型時可以快速從這樣的場景中得到需要的測試數據。因此，在本文中，領域專家首先需要根據規定的場景描述規則撰寫場景，然后在需求模型中執行該場景，驗證需求規約是否正確地描述了期望的場景。

在嵌入式控制軟件領域，存在一些特殊變量，如狀態變量，對于這類變量來說，普通的場景可能不足以驗證它們的性質。此外，由于場景由領域專家手動撰寫，導致效率較低，并且手動撰寫的場景無法保證場景的質量，如果需求覆蓋率較低，則說明場景質量不高，造成分析質量低下。為了解決這些問題，本文從特殊變量場景、效率、場景質量這3 個方面對場景進行優化。

軌道交通控制系統由車載設備和地面設備組成，車載設備和地面設備相互協作保證列車的安全運行。其中車載設備包括列車自動防護（Automatic Train Protection，ATP）系統、列車自動運行（Automatic Train Operation，ATO）系統、列車自動檢測（Automatic Train Supervision，ATS）系統3 個部分。ATP系統是軌道交通系統中的安全控制系統，它通過監控列車速度和各種傳感信號控制列車的運動狀態進行安全控制。ATS系統采集行車信息，實時傳到指揮中心，ATP系統根據ATS給出的信息，按照列車制動能力、列車載重、外部環境等諸多條件計算出列車是否需要減速、制動，并給出最佳方案保證列車的行車安全。ATO系統接收來自ATS和ATP 的信息，控制列車使其在安全范圍內運行，必要時自動制動。ATP系統是一個典型的周期執行系統，它是軌道交通控制軟件的核心，如果發生錯誤會給人們帶來不可估計的生命財產損失，因此保證其安全性和可靠性至關重要。本文以列車自動防護系統（ATP）為例介紹整個需求分析過程。

2 演化式需求建模

在構建形式化需求規約前，首先根據嵌入式控制軟件特點定義需求模板，為領域專家撰寫需求提供指導。

2.1 需求模板

盡管每個軟件系統都有它獨特的特征，但在相似的領域，仍然存在一些相同的特征，這些特征實際上是需求建模的基本元素，需求模板的設計需要滿足這些領域特征。

經研究發現，嵌入式控制軟件大多具有以下特點：1）系統功能基于確定的周期信號運行；2）控制軟件中包含大量全局變量；3）系統明確指定功能的組織，以表示系統架構。這些特點實際上是一些基礎的領域知識，假如為正確且準確的描述這些特點設計一種恰當的機制，那么領域專家可以方便地參與到需求建模過程中。本文通過定義需求模板來指導建立需求規約。需求模板如圖2 所示。所有的領域特點都被組織為模板中的節點和關鍵字，如系統需求可以被描述為功能函數、數據字典和不變量，每個函數的輸入輸出變量都應該在數據字典中指定，前置、后置條件指出了輸入和輸出變量間的關系。根據需求模板，領域專家可以遵循他們傳統的系統需求獲取方式，而不用處理復雜的數學細節。

圖2 ATP系統的需求模板Fig.2 Requirements template of ATP system

2.2 形式化需求規約構建

基于需求模板，可以使用三步演化式的建模方法逐步建立需求規約。

2.2.1 非形式化需求規約構建

在需求規約的構建過程中，需求分析人員更關注全局變量等被多數功能共享的數據資源。特別是對于嵌入式控制軟件來說，在構建非形式化需求規約階段，力求充分地將系統需要的全局變量等數據資源予以描述，對后續工作有重要指引作用。

大多數使用基于模型方法開發的軟件，其開發起點都是需求的獲取和分析。在需求規約建立初期，用戶需求通常是粗糙且不完整的，在這個階段，領域專家和軟件工程師之間頻繁的交流非常重要，因此，在撰寫規約時使用自然語言更合適。非形式化需求文檔的構建是一個初步建立需求描述的過程，在此過程中，需求內容的充分性是首要考量因素，而非需求內容本身的準確性。通過以自然語言書寫需求，不同角色的工程人員可無障礙地參與需求分析過程。圖3 為非形式化需求規約的示例。

圖3 非形式化需求規約示例Fig.3 Example of informal requirement specification

2.2.2 半形式化需求規約構建

構建半形式化需求規約主要思想是對數據結構或系統結構等易于形式化定義的系統特征進行精確描述，而將功能的輸出與輸出變量之間的關系或者軟件時序行為等難以直接用形式化語言描述的特征仍以自然語言描述。這樣的需求文檔可視為形式化和非形式化需求描述方式的一種平衡：既便于程序開發者理解需求，又便于需求分析者檢查文檔。

半形式化的需求文檔側重于對數據結構的形式化定義。在多數嵌入式控制軟件中，存在大量全局變量，需要在需求分析和系統設計早期予以明確。需求分析人員需要形式化定義需求規約中涉及的所有數據結構，并精確定義每個需求條目的輸入輸出變量，最后將需求重新定義為獨立函數。此時，需求規約是一個包含準確接口定義的結構化文件，但每個函數的前置、后置條件仍然是非形式化的。這一過程基于對領域知識和需求的理解，因為明確非形式化需求實際上是一個腦力工作，它依賴于對目標系統中預期功能的理解。圖4 為上述非形式化規約對應的半形式化規約。其中，編號為［SWRQ-0200］的需求被分解為多個函數，每個函數都準確地定義了輸入輸出變量，但它們的前置、后置條件仍然是非形式化的。例如，變量MoOvEsState 是一個枚舉類型變量，WhMaSp 是一個速度單元，被定義在數據字典中。半形式化規約是一個結構化的需求規約，它兼顧了準確性和易讀性，可以方便地進行快速審查和簡單驗證。

圖4 半形式化需求規約示例Fig.4 Example of semi-formal requirement specification

2.2.3 形式化需求規約構建

構建形式化需求規約的主要任務是把半形式化需求規約中的所有組件轉化為形式化規約。此處使用CASDL（CAsco Specification Description Language）［16］形式化語言構建形式化需求規約。這個形式化表示法和Python 語言的風格類似，領域專家和軟件工程師都可以很快掌握它。圖5 為形式化規約示例。

圖5 形式化需求規約示例Fig.5 Example of formal requirement specification

在形式化規約中，每個函數通過定義if-else 條件，形式化的描述了前置、后置條件，即輸入、輸出變量間的關系。為了表示需求變量所在周期，使用了信號變量k。如：需求變量MaMoDuBrOrS1（k）表示變量MaMoDuBrOrS1在當前周期的值，變量MaMoDuBrOrS1（k-1）表示上一周期的值，當變量表示當前周期的值時，k可以省略。

2.3 需求模型導出

需求規約構建完成后，為了進行后續的確認和驗證，需要把形式化規約轉化為可以執行的需求模型。此時，編譯器是必須的，編譯器包括解析器和模型生成器兩部分。解析器把形式化規約轉換為語法分析樹AST（Abstract Syntax Tree），模型生成器通過遍歷AST，把它轉化為需求模型。

本文使用ANTLR（Another Tool for Language Recognition）作為實現解析器的組件。根據給定的語法信息，ANTLR 可以生成解析器解析生成AST，并返回詞法、語法信息。模型生成器使用深度優先遍歷的方法遍歷AST 的每個葉子節點，生成需求模型。需求模型等價于形式化規約，但它更適用于機器讀取。通過分析需求模型，可以生成多個圖表以便驗證需求正確性。算法1 解釋了如何從需求模型中自動導出狀態轉化圖。它以控制流圖CFG（Control Flow Graph）作為輸入，把結構化的數據流轉化為狀態轉化圖。類似地，其他圖表也可以用同樣的方式導出。

3 需求確認和驗證

領域專家更關心它們關注的場景是否正確且充分的被形式化規約描述，而不是一些難以理解的數學符號，需求的確認和驗證應該考慮到領域專家的需要，而不是一個黑盒。因此，在本文中，需求的確認和驗證以領域專家為主導，場景及其預期輸出由領域專家撰寫。

3.1 場景撰寫及執行

首先考慮場景撰寫。對嵌入式控制軟件而言，場景表示的是在一定的時間空間條件下，軟件的載體的狀態，但不同的人看到同一個場景的感覺是不同的。如對ATP系統，在外行人看來，ATP系統是列車的車載設備，其對應的場景是列車的停車、加速、勻速運動等列車運行狀態。而在領域專家的視角下，列車的每一個運行狀態都對應ATP 軟件中的一系列變量的取值。

根據這個特點，本文規定了場景描述規則：每一個場景狀態下都需要給出對應需求規約中的變量取值。例如：在ATP系統中的停車狀態下，需求規約中的變量取值應和停車相符，即此時TrainStop 的取值應為True，而TrainSpeed 的取值應為0。圖6 為場景描述示例，此類場景描述為后面的場景執行提供了便利。

圖6 場景示例Fig.6 Example of scenario

圖6 中‘->’后面的是列車運行動作，括號里的內容為動作參數，它表示的是在當前動作下的量化值。如“start”動作的動作參數是列車起始位置和延遲時間，所有的場景動作定義見表1。在圖6 中，被’’’包圍的是對該運行狀態的解釋，剩下的是需求變量賦值和對應的預期輸出。需求變量的取值應和場景動作相符，如start 動作下的”車輪濾過停止”變量的取值應為True。預期輸出表示的是在場景動作下，待測需求的預期值。

表1 場景動作Tabel 1 Scenario action

表1 中的場景動作1 為領域專家撰寫的場景，為了方便后續的需求變量賦值，本文在對場景邏輯檢查的同時加入了需要的參數信息，即場景動作2。

動態驗證的下一個階段是場景執行。由于規定了場景中必須包括相關需求變量的值，因此在執行需求模型時，測試數據方便的從場景中得到。但由于場景由人手工撰寫，因此難免會漏掉一部分變量，導致場景執行出錯。因此為了保證場景的正確執行，本文規定場景執行時需要遵循以下規則：1）周期執行，即對于周期控制系統，應保持其周期性；2）不影響執行結果原則，即對于沒有輸入數據的變量，在執行時，應根據模型特點對這類變量單獨處理，保證執行結果不受影響。例如：在對ATP系統的驗證中，列車的實際運行場景只有幾個運行狀態變化的場景，而ATP 軟件執行了幾百個周期，因此場景執行時不可能完全模擬現實生活中的列車場景。所以為了保持其周期性，正確的執行場景，列車的每個運行狀態應被看作需求模型的一個周期，對應運行狀態下的需求變量取值應為該狀態執行完畢后相應變量的值。這樣做不僅可以簡化執行周期，縮短場景撰寫時間，而且不會影響執行結果。

3.2 場景優化

為了進一步驗證嵌入式控制軟件的正確性，本文提出了場景優化方法。首先在大多數的嵌入式控制軟件中，都存在模式變化。對于這類表示模式變化的特殊變量，如狀態變量，不同狀態間的轉化關系需要嚴格定義，因此普通的場景不足以滿足對這類特殊變量的驗證。其次，在本文方法中，場景由領域專家手工撰寫，導致效率不高。最后，在本方法中，場景的質量高低對整個驗證結果有較大的影響。因此本文從特殊變量的場景優化、效率優化和場景質量優化這3 個方面優化場景。

下文將以列車自動防護系統（ATP）為例具體介紹場景優化方法。

3.2.1 特殊變量的場景優化

在對特殊變量的場景優化中，本文主要考慮狀態變量的優化，從領域專家的角度來看，狀態變量的如下性質需要被滿足：

性質1無二義轉化，對每個系統狀態，每周期只能有一個狀態轉化條件被滿足。

上述性質在嵌入式控制軟件中是非常普遍的。它表示對任意一個狀態變量來說，雖然存在多個轉化條件，但要求在任意一個周期內，只有一個條件是被滿足的，否則，系統的行為將會不可確定。

為保證狀態轉化的無二義性，各個狀態間的轉化條件應該是互斥的。本文從以下3 個步驟判斷轉化條件是否是互斥的：1）收集轉化條件；2）通過兩兩組合，組成轉化條件對；3）使用z3 求解器檢查每對條件是否可以同時被滿足。

圖7 所示為列車運動打滑控制狀態轉化圖，從中可以查看每個狀態間的關系。顯然，當一個狀態和m個轉化條件相連時，有m（m－1）/2 個條件組合需要被檢查。

圖7 狀態轉化圖示例Fig.7 Example of state transition diagram

對條件組合的檢查實際上是一個約束求解問題，如果一對條件有解，則說明它們不互斥，即狀態轉化是不正確的。本文使用z3 求解器求解這個約束問題，如果z3 求解器求解條件對的返回值是UNSATISFIABLE，則證明這2 個條件互斥，符合要求。

從狀態SLIDING 轉化到其他狀態時的轉化條件C1、C2、C3 如下：

這3 個轉化條件組成了3 個條件組合：C1&&C 2，C1&&C3，C2&&C3，把它們代入Z3 求解器中求解，Z3 求解器的返回值是UNSATISFIABLE。所以這表明狀態SLIDING 的轉化條件是互斥的。

3.2.2 效率優化

為提高需求驗證的效率，本文提出一種效率優化方法――自動生成場景。如在ATP系統中，自動生成列車場景中的列車運行狀態和需求變量部分。自動生成場景時無需手動計算動作參數中的量化數據，并且場景中的需求變量賦值部分可以根據場景動作、動作參數和變量賦值規則自動生成。事實證明，這樣可以提高驗證效率。

在自動生成場景時，首先獲取待測需求的所有輸入；然后自動生成列車運行時的場景動作；最后根據變量賦值規則生成變量賦值部分。具體的場景生成方法如圖8 所示。

圖8 自動生成場景流程Fig.8 Flow chart of automatically scenario generation

首先考慮自動生成場景動作。在表1 的場景動作中，不同的動作的參數不同。如勻速動作的動作參數只有“勻速運行時間”一個參數，而加速動作參數中必須有“加速度”。因此本文根據場景動作的特點，自動生成對應參數，并計算此時的位置、速度等信息，方便后續需求變量賦值。具體的場景動作生成過程見算法2，其中，邏輯檢查的目的是保證動作參數的值不能超過規定區間。本文使用速度公式和加速度公式計算列車的速度和加速度，并確保這些值在領域專家規定的最大范圍內。

接下來考慮需求變量賦值。為了保證變量賦值的合理性，經研究發現，需求變量的取值與所在場景動作和場景序列的順序有關，根據這個特點，本文定義了變量賦值規則，主要包括場景情景和變量賦值，具體見表2和表3 所示。其中，“場景情境”表示的是需求變量在不同的情境下應該如何賦值，“變量賦值”指的是不同類型變量應該如何賦值。根據變量賦值規則可以自動生成場景中的需求變量賦值部分。

表2 場景情境賦值內容Table 2 Assignment of scene situation

表3 變量賦值規則Table 3 Variable assignment rules

3.2.3 場景質量優化

領域專家撰寫的場景，如果只能覆蓋較少的一部分需求，則難以確定其他未被覆蓋的需求是否正確地描述了預期的場景，造成分析質量低下。由于場景由領域專家撰寫，因此，本文通過為領域專家撰寫場景提供參考的方法，達到優化場景質量的目的。具體過程如下：1）求解未覆蓋路徑；2）生成未覆蓋路徑對應的測試用例。

未覆蓋需求對應的測試用例為領域專家撰寫場景提供參考。首先考慮未覆蓋路徑的生成。執行需求模型后，可以得到每個場景中的各個周期的需求覆蓋行和整個場景的需求覆蓋率。根據場景的需求覆蓋情況，可以從中得到覆蓋行和未覆蓋行，通過向上追溯未覆蓋語句的直接判斷條件、間接判斷條件，可以得到需求未覆蓋路徑。算法3 為未覆蓋路徑具體生成過程。其中cfg.mark 是覆蓋語句標志，當它的取值為－1 時，表示該語句未被覆蓋，其對應的判斷條件及前置條件為未覆蓋路徑。

接下來生成未覆蓋路徑對應的測試用例。本文在生成測試用例時，采用MC/DC 覆蓋準則，其廣泛應用于嵌入式系統控制軟件。MC/DC（Modified Condition/Decision Coverage）修正的判定條件覆蓋準則，要求首先實現條件覆蓋（每個判斷中每個條件的可能取值至少滿足一次）和判定覆蓋（程序中的每一個判斷至少獲得一次“真”或“假”），并在此基礎上，每個判定中的條件必須獨立影響一個判定的輸出。獨立影響的意思是在其他條件不變的情況下，改變條件C1 的取值，判定結果也會隨之改變。

算法4為測試用例生成算法，MCDC 函數的輸入有表達式、前置條件。在求解測試用例時，為了實現MCDC中的獨立影響原則，需要反復迭代計算判斷條件。

3.3 需求確認和驗證

本文目標是動態地驗證需求規約是否準確且充分描述了期望的場景。領域專家首先撰寫相應場景，然后根據場景中的數據信息執行需求模型，最后判斷需求規約是否正確地描述了該場景，驗證需求正確性。通過場景優化，可以提高整個驗證效率，提高需求分析的質量。其中，通過驗證狀態轉化條件的互斥性，保證了狀態轉化的唯一性。這些特殊變量往往貫穿于嵌入式控制軟件的整個需求中，因此，對它們進行更嚴格的驗證是必要的。

4 實驗與結果分析

為評估本文方法的可行性，在CASCO 的ATP 項目中應用了需求建模和需求確認和驗證。ATP系統的形式化需求規約由450 個功能函數組成，其中，為動態需求確認和驗證生成了8 個狀態轉換圖，對狀態變量進行了更嚴格的驗證。

為驗證需求規約是否正確描述了期望的場景，通過執行領域專家撰寫的場景，筆者發現了2 個需求錯誤。在對狀態變量的驗證中，發現了3 個“無二義轉化”錯誤。除了狀態轉換圖，還生成了300 個變量依賴圖，以進行嚴格審查。通過變量依賴圖，領域專家可以追溯和當前變量相關的所有變量，驗證變量間的依賴關系是否符合要求。如果變量a的取值依賴于變量b、c的值，而在需求描述中，它的取值還和變量d有關，顯然這種依賴關系是錯誤的。

本文方法還提高了需求建模和需求確認和驗證的效率。具體結果見表4。可以看出，與傳統的正式規約構建相比，使用演化式需求建模方法構建形式化需求規約的時間成本從3 個月減少到不到2 個月。其中，自動生成場景的方法可以大幅提高場景撰寫的效率，手工撰寫一條場景可能需要5 min～10 min的時間，而自動生成多條場景只需幾秒鐘。本文還驗證了8 個狀態變量的性質，與手動驗證相比，驗證時間從1 h～2 h 縮減到2 s。由于各種因素，例如：用戶的經驗或項目內容的不同，這種改進可能會有所不同。盡管如此，本文方法仍有助于驗證驗證需求正確性，從而可以發現更多潛在的錯誤。

表4 實驗結果比較Table 4 Comparsion of experimental result

未覆蓋路徑及測試用例生成為測試人員撰寫高質量場景提供了幫助。為了提高場景的質量，在一般情況下，測試人員需要先找到未覆蓋語句，向上追溯未覆蓋路徑，分析需求未覆蓋原因，從而撰寫高質量的場景。本文方法為測試人員分析未覆蓋原因節省了手動推導未覆蓋路徑的過程，并且測試用例的生成進一步為分析未覆蓋原因提供條件。在表4中，根據場景執行結果，在450個需求條目中生成了60條未覆蓋路徑及測試用例，與手動分析相比，大幅縮短了未覆蓋路徑推導時間。

在整個需求驗證過程中，需求建模往往需要耗費更多的時間，而當需求變更時，模型改動也較復雜，因此，如果能用有效的建模方法更快的建立需求模型，就可以大幅提高整個需求驗證效率。在對場景的優化方面，本文通過自動生成場景，解決了在撰寫場景過程中大量重復的物理計算問題，使領域專家可以重點關注領域專業相關的內容。

如在ATP系統中的列車運動打滑控制模塊中，其需求描述中存在速度、加速度，如“進入可補償的打滑狀態時速度”“瞬時加速度”“平均加速度”等變量，如果場景要盡可能多的覆蓋需求時，則需要考慮到不同的速度、加速度組合才能滿足不同的判斷條件。在我們的方法中，通過自動生成場景，可以省去大量的重復計算。

而當場景在需求模型中執行結束后，可以知道需求中哪一部分的內容沒有被覆蓋，為了驗證這部分未覆蓋需求的正確性，則需要分析需求未覆蓋原因，撰寫對應場景。在這個過程中，領域專家首先需要找到未覆蓋需求，然后找到和該未覆蓋行相關的所有判斷條件，最后需要在判斷條件中分析每個變量對場景的影響，從而撰寫出對應的場景。這個過程中的一些重復操作可以自動完成，因此本文方法根據需求覆蓋情況自動生成了未覆蓋路徑及其對應的測試用例。在圖9 中的未覆蓋路徑示例中，為了滿足判斷條件，需要經過計算才能得到每個需求變量的取值。本文基于MC/DC 覆蓋準則生成未覆蓋路徑對應的測試用例，如圖10 所示，為領域專家分析需求未覆蓋原因提供了幫助。

圖9 未覆蓋路徑示例Fig.9 Example of uncovered path

圖10 測試用例示例Fig.10 Example of test case

實驗結果表明，本文方法可以有效地幫助嵌入式控制軟件領域的領域專家改善需求建模和分析。它使從業人員可以有效地構建形式化的需求規約，而不是使用非形式化的規格說明進行分析需求。根據精確的形式化規約，將自動檢測更多錯誤。從時間成本的角度來看，建立形式化規約可能會花費一些時間。根據領域專家的反饋，這種方法的一個重要優勢是“考慮了特定領域的知識和功能”。與傳統的形式化方法相比，這種方法可以使領域專家參與整個需求建模和需求確認和驗證過程。在構建形式化需求規約時，它直接告訴從業人員“做什么”和“怎么做”，而不是只給出復雜的符號和形式化證明規則。另一個重要的方面是“工程過程”，它以連貫的方式結合了演化式需求建模和基于場景的需求確認和驗證。

5 結束語

本文面向嵌入式控制領域提出一種基于場景的需求確認和驗證方法。利用領域知識和特征設計需求模板，在模板指導下構建需求規約，并使用三步演化式建模方法逐步構建形式化的需求規約，導出需求模型，同時生成需求確認和驗證需要的各種圖表。在此基礎上，領域專家根據規則撰寫場景。通過執行場景，領域專家可以判斷需求規約是否正確的描述了期望的場景。本文通過設計特殊場景，驗證了特殊變量的正確性；通過自動生成場景，提高了需求驗證的效率；并通過求解未覆蓋路徑及測試用例，為提高場景質量提供了幫助。實驗結果證明了本文方法的可行性。未來將對場景做進一步優化以適用更多情況，如給出場景撰寫規則以提高場景質量。