閆倩倩，繆煒愷

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

0 概述

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

然而，如何把形式化方法應(yīng)用到真實的工業(yè)軟件中依然是一大挑戰(zhàn)［4］。首先，目前缺乏建立形式化規(guī)約的方法。一方面，由于軟件需求大多使用自然語言撰寫而自然語言描述具有不準(zhǔn)確性，軟件工程師在構(gòu)建需求規(guī)約時未必能準(zhǔn)確且精確地描述系統(tǒng)功能；另一方面，領(lǐng)域?qū)＜規(guī)缀醪豢赡苁褂脧?fù)雜的形式化表示法描述系統(tǒng)需求，多數(shù)領(lǐng)域?qū)＜胰鄙賵詫嵉碾x散數(shù)學(xué)基礎(chǔ)，并且學(xué)習(xí)復(fù)雜的數(shù)學(xué)符號和證明技巧既費(fèi)時又費(fèi)力。其次，形式化的需求確認(rèn)和驗證大多由軟件工程師主導(dǎo)，缺乏領(lǐng)域?qū)＜乙暯?。傳統(tǒng)的形式化驗證側(cè)重于使用形式化證明方法發(fā)現(xiàn)軟件中的邏輯錯誤，如不一致性，但這對領(lǐng)域?qū)＜襾碚f是難以理解的。

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

場景是一種用于分析軟件的重要途徑，且符合領(lǐng)域?qū)＜业乃季S方式。在基于場景的設(shè)計分析方面，基于模型驅(qū)動的方式被廣泛使用?；趫鼍暗腃BTC（Communication Based Train Control）系統(tǒng)建模［25］方法，通過場景模型和需求間的追溯關(guān)系，指導(dǎo)如何撰寫場景的方法［26］，用一階線性邏輯驗證需求場景的正確性等方法［27］。目前，研究人員大都關(guān)注軟件代碼功能，生成測試用例，給出優(yōu)化方法［28-29］。然而這些方法都沒有提供一個基于物理場景的需求確認(rèn)和驗證方法。

本文針對面向軌道交通領(lǐng)域的嵌入式控制軟件，提出一種以領(lǐng)域?qū)＜覟橹行牡幕趫鼍暗男枨蠓治龇椒?。使用三步演化式建模方法建立形式化的需求?guī)約，避免復(fù)雜的數(shù)學(xué)運(yùn)算，并導(dǎo)出需求模型。在此基礎(chǔ)上，領(lǐng)域?qū)＜腋鶕?jù)規(guī)則撰寫場景分析場景執(zhí)行結(jié)果驗證需求規(guī)約是否正確地描述了期望的場景。為驗證需求的正確性，提高需求確認(rèn)和驗證的效率，分別從特殊變量場景、效率、場景質(zhì)量這3 個方面對場景進(jìn)行優(yōu)化。

1 方法框架

如圖1 所示，本文方法主要包括演化式需求建模和需求的確認(rèn)和驗證2 個部分。首先，通過和領(lǐng)域?qū)＜业拇罅拷涣?，從嵌入式控制軟件中提取特定領(lǐng)域的特征，并根據(jù)這些周期性、模式轉(zhuǎn)化等特征，建立需求規(guī)約模板，領(lǐng)域?qū)＜铱梢愿鶕?jù)模板的指導(dǎo)使用自然語言構(gòu)建非形式化規(guī)約，軟件工程師和領(lǐng)域?qū)＜叶伎梢钥焖俚乩斫夥切问交枨?；然后，在非形式化需求被確認(rèn)后，非形式化需求被轉(zhuǎn)化為半形式化需求，所有的數(shù)據(jù)結(jié)構(gòu)都被形式化的定義，在這個階段，系統(tǒng)結(jié)構(gòu)仍然可以被方便的修改重塑；最后，當(dāng)半形式化規(guī)約確認(rèn)后，用戶需求被最終轉(zhuǎn)化為形式化地需求規(guī)約，此時，所有的變量、功能都被形式化地定義。

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

需求形式化規(guī)約構(gòu)建完成后，接下來驗證需求正確性，需求規(guī)約首先被轉(zhuǎn)化為形式化需求模型。在嵌入式控制軟件領(lǐng)域，傳統(tǒng)的基于場景的測試方法是把場景放到仿真平臺上執(zhí)行，然而對大規(guī)模的嵌入式軟件來說，為了驗證其中一個子系統(tǒng)的需求正確性，仿真執(zhí)行時需要配置大量初始信息，費(fèi)時費(fèi)力。設(shè)想，如果場景能直接在需求模型中執(zhí)行，則可以節(jié)約大量時間資源。為此，本文規(guī)定場景描述規(guī)則，即在場景中加入相關(guān)需求變量的取值，從而在執(zhí)行需求模型時可以快速從這樣的場景中得到需要的測試數(shù)據(jù)。因此，在本文中，領(lǐng)域?qū)＜沂紫刃枰鶕?jù)規(guī)定的場景描述規(guī)則撰寫場景，然后在需求模型中執(zhí)行該場景，驗證需求規(guī)約是否正確地描述了期望的場景。

在嵌入式控制軟件領(lǐng)域，存在一些特殊變量，如狀態(tài)變量，對于這類變量來說，普通的場景可能不足以驗證它們的性質(zhì)。此外，由于場景由領(lǐng)域?qū)＜沂謩幼珜?，?dǎo)致效率較低，并且手動撰寫的場景無法保證場景的質(zhì)量，如果需求覆蓋率較低，則說明場景質(zhì)量不高，造成分析質(zhì)量低下。為了解決這些問題，本文從特殊變量場景、效率、場景質(zhì)量這3 個方面對場景進(jìn)行優(yōu)化。

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

2 演化式需求建模

在構(gòu)建形式化需求規(guī)約前，首先根據(jù)嵌入式控制軟件特點定義需求模板，為領(lǐng)域?qū)＜易珜懶枨筇峁┲笇?dǎo)。

2.1 需求模板

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

經(jīng)研究發(fā)現(xiàn)，嵌入式控制軟件大多具有以下特點：1）系統(tǒng)功能基于確定的周期信號運(yùn)行；2）控制軟件中包含大量全局變量；3）系統(tǒng)明確指定功能的組織，以表示系統(tǒng)架構(gòu)。這些特點實際上是一些基礎(chǔ)的領(lǐng)域知識，假如為正確且準(zhǔn)確的描述這些特點設(shè)計一種恰當(dāng)?shù)臋C(jī)制，那么領(lǐng)域?qū)＜铱梢苑奖愕貐⑴c到需求建模過程中。本文通過定義需求模板來指導(dǎo)建立需求規(guī)約。需求模板如圖2 所示。所有的領(lǐng)域特點都被組織為模板中的節(jié)點和關(guān)鍵字，如系統(tǒng)需求可以被描述為功能函數(shù)、數(shù)據(jù)字典和不變量，每個函數(shù)的輸入輸出變量都應(yīng)該在數(shù)據(jù)字典中指定，前置、后置條件指出了輸入和輸出變量間的關(guān)系。根據(jù)需求模板，領(lǐng)域?qū)＜铱梢宰裱麄儌鹘y(tǒng)的系統(tǒng)需求獲取方式，而不用處理復(fù)雜的數(shù)學(xué)細(xì)節(jié)。

圖2 ATP系統(tǒng)的需求模板Fig.2 Requirements template of ATP system

2.2 形式化需求規(guī)約構(gòu)建

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

2.2.1 非形式化需求規(guī)約構(gòu)建

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

大多數(shù)使用基于模型方法開發(fā)的軟件，其開發(fā)起點都是需求的獲取和分析。在需求規(guī)約建立初期，用戶需求通常是粗糙且不完整的，在這個階段，領(lǐng)域?qū)＜液蛙浖こ處熤g頻繁的交流非常重要，因此，在撰寫規(guī)約時使用自然語言更合適。非形式化需求文檔的構(gòu)建是一個初步建立需求描述的過程，在此過程中，需求內(nèi)容的充分性是首要考量因素，而非需求內(nèi)容本身的準(zhǔn)確性。通過以自然語言書寫需求，不同角色的工程人員可無障礙地參與需求分析過程。圖3 為非形式化需求規(guī)約的示例。

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

2.2.2 半形式化需求規(guī)約構(gòu)建

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

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

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

2.2.3 形式化需求規(guī)約構(gòu)建

構(gòu)建形式化需求規(guī)約的主要任務(wù)是把半形式化需求規(guī)約中的所有組件轉(zhuǎn)化為形式化規(guī)約。此處使用CASDL（CAsco Specification Description Language）［16］形式化語言構(gòu)建形式化需求規(guī)約。這個形式化表示法和Python 語言的風(fēng)格類似，領(lǐng)域?qū)＜液蛙浖こ處煻伎梢院芸煺莆账?。圖5 為形式化規(guī)約示例。

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

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

2.3 需求模型導(dǎo)出

需求規(guī)約構(gòu)建完成后，為了進(jìn)行后續(xù)的確認(rèn)和驗證，需要把形式化規(guī)約轉(zhuǎn)化為可以執(zhí)行的需求模型。此時，編譯器是必須的，編譯器包括解析器和模型生成器兩部分。解析器把形式化規(guī)約轉(zhuǎn)換為語法分析樹AST（Abstract Syntax Tree），模型生成器通過遍歷AST，把它轉(zhuǎn)化為需求模型。

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

3 需求確認(rèn)和驗證

領(lǐng)域?qū)＜腋P(guān)心它們關(guān)注的場景是否正確且充分的被形式化規(guī)約描述，而不是一些難以理解的數(shù)學(xué)符號，需求的確認(rèn)和驗證應(yīng)該考慮到領(lǐng)域?qū)＜业男枰?，而不是一個黑盒。因此，在本文中，需求的確認(rèn)和驗證以領(lǐng)域?qū)＜覟橹鲗?dǎo)，場景及其預(yù)期輸出由領(lǐng)域?qū)＜易珜憽?/p>

3.1 場景撰寫及執(zhí)行

首先考慮場景撰寫。對嵌入式控制軟件而言，場景表示的是在一定的時間空間條件下，軟件的載體的狀態(tài)，但不同的人看到同一個場景的感覺是不同的。如對ATP系統(tǒng)，在外行人看來，ATP系統(tǒng)是列車的車載設(shè)備，其對應(yīng)的場景是列車的停車、加速、勻速運(yùn)動等列車運(yùn)行狀態(tài)。而在領(lǐng)域?qū)＜业囊暯窍?，列車的每一個運(yùn)行狀態(tài)都對應(yīng)ATP 軟件中的一系列變量的取值。

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

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

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

表1 場景動作Tabel 1 Scenario action

表1 中的場景動作1 為領(lǐng)域?qū)＜易珜懙膱鼍?，為了方便后續(xù)的需求變量賦值，本文在對場景邏輯檢查的同時加入了需要的參數(shù)信息，即場景動作2。

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

3.2 場景優(yōu)化

為了進(jìn)一步驗證嵌入式控制軟件的正確性，本文提出了場景優(yōu)化方法。首先在大多數(shù)的嵌入式控制軟件中，都存在模式變化。對于這類表示模式變化的特殊變量，如狀態(tài)變量，不同狀態(tài)間的轉(zhuǎn)化關(guān)系需要嚴(yán)格定義，因此普通的場景不足以滿足對這類特殊變量的驗證。其次，在本文方法中，場景由領(lǐng)域?qū)＜沂止ぷ珜懀瑢?dǎo)致效率不高。最后，在本方法中，場景的質(zhì)量高低對整個驗證結(jié)果有較大的影響。因此本文從特殊變量的場景優(yōu)化、效率優(yōu)化和場景質(zhì)量優(yōu)化這3 個方面優(yōu)化場景。

下文將以列車自動防護(hù)系統(tǒng)（ATP）為例具體介紹場景優(yōu)化方法。

3.2.1 特殊變量的場景優(yōu)化

在對特殊變量的場景優(yōu)化中，本文主要考慮狀態(tài)變量的優(yōu)化，從領(lǐng)域?qū)＜业慕嵌葋砜?，狀態(tài)變量的如下性質(zhì)需要被滿足：

性質(zhì)1無二義轉(zhuǎn)化，對每個系統(tǒng)狀態(tài)，每周期只能有一個狀態(tài)轉(zhuǎn)化條件被滿足。

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

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

圖7 所示為列車運(yùn)動打滑控制狀態(tài)轉(zhuǎn)化圖，從中可以查看每個狀態(tài)間的關(guān)系。顯然，當(dāng)一個狀態(tài)和m個轉(zhuǎn)化條件相連時，有m（m－1）/2 個條件組合需要被檢查。

圖7 狀態(tài)轉(zhuǎn)化圖示例Fig.7 Example of state transition diagram

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

從狀態(tài)SLIDING 轉(zhuǎn)化到其他狀態(tài)時的轉(zhuǎn)化條件C1、C2、C3 如下：

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

3.2.2 效率優(yōu)化

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

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

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

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

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

表2 場景情境賦值內(nèi)容Table 2 Assignment of scene situation

表3 變量賦值規(guī)則Table 3 Variable assignment rules

3.2.3 場景質(zhì)量優(yōu)化

領(lǐng)域?qū)＜易珜懙膱鼍?，如果只能覆蓋較少的一部分需求，則難以確定其他未被覆蓋的需求是否正確地描述了預(yù)期的場景，造成分析質(zhì)量低下。由于場景由領(lǐng)域?qū)＜易珜?，因此，本文通過為領(lǐng)域?qū)＜易珜憟鼍疤峁﹨⒖嫉姆椒ǎ_(dá)到優(yōu)化場景質(zhì)量的目的。具體過程如下：1）求解未覆蓋路徑；2）生成未覆蓋路徑對應(yīng)的測試用例。

未覆蓋需求對應(yīng)的測試用例為領(lǐng)域?qū)＜易珜憟鼍疤峁﹨⒖肌Ｊ紫瓤紤]未覆蓋路徑的生成。執(zhí)行需求模型后，可以得到每個場景中的各個周期的需求覆蓋行和整個場景的需求覆蓋率。根據(jù)場景的需求覆蓋情況，可以從中得到覆蓋行和未覆蓋行，通過向上追溯未覆蓋語句的直接判斷條件、間接判斷條件，可以得到需求未覆蓋路徑。算法3 為未覆蓋路徑具體生成過程。其中cfg.mark 是覆蓋語句標(biāo)志，當(dāng)它的取值為－1 時，表示該語句未被覆蓋，其對應(yīng)的判斷條件及前置條件為未覆蓋路徑。

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

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

3.3 需求確認(rèn)和驗證

本文目標(biāo)是動態(tài)地驗證需求規(guī)約是否準(zhǔn)確且充分描述了期望的場景。領(lǐng)域?qū)＜沂紫茸珜懴鄳?yīng)場景，然后根據(jù)場景中的數(shù)據(jù)信息執(zhí)行需求模型，最后判斷需求規(guī)約是否正確地描述了該場景，驗證需求正確性。通過場景優(yōu)化，可以提高整個驗證效率，提高需求分析的質(zhì)量。其中，通過驗證狀態(tài)轉(zhuǎn)化條件的互斥性，保證了狀態(tài)轉(zhuǎn)化的唯一性。這些特殊變量往往貫穿于嵌入式控制軟件的整個需求中，因此，對它們進(jìn)行更嚴(yán)格的驗證是必要的。

4 實驗與結(jié)果分析

為評估本文方法的可行性，在CASCO 的ATP 項目中應(yīng)用了需求建模和需求確認(rèn)和驗證。ATP系統(tǒng)的形式化需求規(guī)約由450 個功能函數(shù)組成，其中，為動態(tài)需求確認(rèn)和驗證生成了8 個狀態(tài)轉(zhuǎn)換圖，對狀態(tài)變量進(jìn)行了更嚴(yán)格的驗證。

為驗證需求規(guī)約是否正確描述了期望的場景，通過執(zhí)行領(lǐng)域?qū)＜易珜懙膱鼍?，筆者發(fā)現(xiàn)了2 個需求錯誤。在對狀態(tài)變量的驗證中，發(fā)現(xiàn)了3 個“無二義轉(zhuǎn)化”錯誤。除了狀態(tài)轉(zhuǎn)換圖，還生成了300 個變量依賴圖，以進(jìn)行嚴(yán)格審查。通過變量依賴圖，領(lǐng)域?qū)＜铱梢宰匪莺彤?dāng)前變量相關(guān)的所有變量，驗證變量間的依賴關(guān)系是否符合要求。如果變量a的取值依賴于變量b、c的值，而在需求描述中，它的取值還和變量d有關(guān)，顯然這種依賴關(guān)系是錯誤的。

本文方法還提高了需求建模和需求確認(rèn)和驗證的效率。具體結(jié)果見表4?？梢钥闯觯c傳統(tǒng)的正式規(guī)約構(gòu)建相比，使用演化式需求建模方法構(gòu)建形式化需求規(guī)約的時間成本從3 個月減少到不到2 個月。其中，自動生成場景的方法可以大幅提高場景撰寫的效率，手工撰寫一條場景可能需要5 min～10 min的時間，而自動生成多條場景只需幾秒鐘。本文還驗證了8 個狀態(tài)變量的性質(zhì)，與手動驗證相比，驗證時間從1 h～2 h 縮減到2 s。由于各種因素，例如：用戶的經(jīng)驗或項目內(nèi)容的不同，這種改進(jìn)可能會有所不同。盡管如此，本文方法仍有助于驗證驗證需求正確性，從而可以發(fā)現(xiàn)更多潛在的錯誤。

表4 實驗結(jié)果比較Table 4 Comparsion of experimental result

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

在整個需求驗證過程中，需求建模往往需要耗費(fèi)更多的時間，而當(dāng)需求變更時，模型改動也較復(fù)雜，因此，如果能用有效的建模方法更快的建立需求模型，就可以大幅提高整個需求驗證效率。在對場景的優(yōu)化方面，本文通過自動生成場景，解決了在撰寫場景過程中大量重復(fù)的物理計算問題，使領(lǐng)域?qū)＜铱梢灾攸c關(guān)注領(lǐng)域?qū)I(yè)相關(guān)的內(nèi)容。

如在ATP系統(tǒng)中的列車運(yùn)動打滑控制模塊中，其需求描述中存在速度、加速度，如“進(jìn)入可補(bǔ)償?shù)拇蚧瑺顟B(tài)時速度”“瞬時加速度”“平均加速度”等變量，如果場景要盡可能多的覆蓋需求時，則需要考慮到不同的速度、加速度組合才能滿足不同的判斷條件。在我們的方法中，通過自動生成場景，可以省去大量的重復(fù)計算。

而當(dāng)場景在需求模型中執(zhí)行結(jié)束后，可以知道需求中哪一部分的內(nèi)容沒有被覆蓋，為了驗證這部分未覆蓋需求的正確性，則需要分析需求未覆蓋原因，撰寫對應(yīng)場景。在這個過程中，領(lǐng)域?qū)＜沂紫刃枰业轿锤采w需求，然后找到和該未覆蓋行相關(guān)的所有判斷條件，最后需要在判斷條件中分析每個變量對場景的影響，從而撰寫出對應(yīng)的場景。這個過程中的一些重復(fù)操作可以自動完成，因此本文方法根據(jù)需求覆蓋情況自動生成了未覆蓋路徑及其對應(yīng)的測試用例。在圖9 中的未覆蓋路徑示例中，為了滿足判斷條件，需要經(jīng)過計算才能得到每個需求變量的取值。本文基于MC/DC 覆蓋準(zhǔn)則生成未覆蓋路徑對應(yīng)的測試用例，如圖10 所示，為領(lǐng)域?qū)＜曳治鲂枨笪锤采w原因提供了幫助。

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

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

實驗結(jié)果表明，本文方法可以有效地幫助嵌入式控制軟件領(lǐng)域的領(lǐng)域?qū)＜腋纳菩枨蠼：头治?。它使從業(yè)人員可以有效地構(gòu)建形式化的需求規(guī)約，而不是使用非形式化的規(guī)格說明進(jìn)行分析需求。根據(jù)精確的形式化規(guī)約，將自動檢測更多錯誤。從時間成本的角度來看，建立形式化規(guī)約可能會花費(fèi)一些時間。根據(jù)領(lǐng)域?qū)＜业姆答?，這種方法的一個重要優(yōu)勢是“考慮了特定領(lǐng)域的知識和功能”。與傳統(tǒng)的形式化方法相比，這種方法可以使領(lǐng)域?qū)＜覅⑴c整個需求建模和需求確認(rèn)和驗證過程。在構(gòu)建形式化需求規(guī)約時，它直接告訴從業(yè)人員“做什么”和“怎么做”，而不是只給出復(fù)雜的符號和形式化證明規(guī)則。另一個重要的方面是“工程過程”，它以連貫的方式結(jié)合了演化式需求建模和基于場景的需求確認(rèn)和驗證。

5 結(jié)束語

本文面向嵌入式控制領(lǐng)域提出一種基于場景的需求確認(rèn)和驗證方法。利用領(lǐng)域知識和特征設(shè)計需求模板，在模板指導(dǎo)下構(gòu)建需求規(guī)約，并使用三步演化式建模方法逐步構(gòu)建形式化的需求規(guī)約，導(dǎo)出需求模型，同時生成需求確認(rèn)和驗證需要的各種圖表。在此基礎(chǔ)上，領(lǐng)域?qū)＜腋鶕?jù)規(guī)則撰寫場景。通過執(zhí)行場景，領(lǐng)域?qū)＜铱梢耘袛嘈枨笠?guī)約是否正確的描述了期望的場景。本文通過設(shè)計特殊場景，驗證了特殊變量的正確性；通過自動生成場景，提高了需求驗證的效率；并通過求解未覆蓋路徑及測試用例，為提高場景質(zhì)量提供了幫助。實驗結(jié)果證明了本文方法的可行性。未來將對場景做進(jìn)一步優(yōu)化以適用更多情況，如給出場景撰寫規(guī)則以提高場景質(zhì)量。