閆倩倩，繆煒愷

（華東師范大學(xué)上海市高可信計(jì)算重點(diǎn)實(shí)驗(yàn)室，上海 200062）

0 概述

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

然而，如何把形式化方法應(yīng)用到真實(shí)的工業(yè)軟件中依然是一大挑戰(zhàn)［4］。首先，目前缺乏建立形式化規(guī)約的方法。一方面，由于軟件需求大多使用自然語言撰寫而自然語言描述具有不準(zhǔn)確性，軟件工程師在構(gòu)建需求規(guī)約時(shí)未必能準(zhǔn)確且精確地描述系統(tǒng)功能；另一方面，領(lǐng)域?qū)＜規(guī)缀醪豢赡苁褂脧?fù)雜的形式化表示法描述系統(tǒng)需求，多數(shù)領(lǐng)域?qū)＜胰鄙賵?jiān)實(shí)的離散數(shù)學(xué)基礎(chǔ)，并且學(xué)習(xí)復(fù)雜的數(shù)學(xué)符號(hào)和證明技巧既費(fèi)時(shí)又費(fèi)力。其次，形式化的需求確認(rèn)和驗(yàn)證大多由軟件工程師主導(dǎo)，缺乏領(lǐng)域?qū)＜乙暯?。傳統(tǒng)的形式化驗(yàn)證側(cè)重于使用形式化證明方法發(fā)現(xiàn)軟件中的邏輯錯(cuò)誤，如不一致性，但這對(duì)領(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］等。而在需求分析階段，需求審查因其易推廣、實(shí)施容易的特點(diǎn)，廣泛應(yīng)用于需求確認(rèn)過程中。研究人員提出了一系列需求審查方法，如基于查詢模型的提問式審查方法［13］、以認(rèn)知模型為基礎(chǔ)的審查方法［14］、以虛擬原型為基礎(chǔ)的審查方法［15］等。規(guī)約測(cè)試技術(shù)也是一種經(jīng)常應(yīng)用于需求確認(rèn)的方法。VDMTools 工具［16］執(zhí)行用VDM 語言寫成的規(guī)約顯示系統(tǒng)動(dòng)作供測(cè)試人員確認(rèn)。同時(shí)，ProB 為B 語言需求規(guī)約提供一種確認(rèn)手段［17］。模型檢查也是一種常用的形式化分析方法，如：基于特定語言的建模方法DSL［18-19］；一種用EAST-ADL 描述的架構(gòu)模型分析技術(shù)［20］，包括EAST-ADL 的模擬執(zhí)行；基于組件的BIP 模型被用來進(jìn)行軟件建模和驗(yàn)證［21］，用于對(duì)無界時(shí)間屬性的馬爾可夫鏈進(jìn)行統(tǒng)計(jì)模型檢查的算法［22］等。在工業(yè)上的應(yīng)用方面，StateChart 廣泛應(yīng)用于工業(yè)軟件建模和分析［23］，Matlab/Simulink 提供了Stateflow［24］。然而這些方法都沒有為大型工業(yè)項(xiàng)目提供一個(gè)系統(tǒng)的需求建模方法。

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

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

1 方法框架

如圖1 所示，本文方法主要包括演化式需求建模和需求的確認(rèn)和驗(yàn)證2 個(gè)部分。首先，通過和領(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)都被形式化的定義，在這個(gè)階段，系統(tǒng)結(jié)構(gòu)仍然可以被方便的修改重塑；最后，當(dāng)半形式化規(guī)約確認(rèn)后，用戶需求被最終轉(zhuǎn)化為形式化地需求規(guī)約，此時(shí)，所有的變量、功能都被形式化地定義。

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

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

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

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

2 演化式需求建模

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

2.1 需求模板

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

經(jīng)研究發(fā)現(xiàn)，嵌入式控制軟件大多具有以下特點(diǎn)：1）系統(tǒng)功能基于確定的周期信號(hào)運(yùn)行；2）控制軟件中包含大量全局變量；3）系統(tǒng)明確指定功能的組織，以表示系統(tǒng)架構(gòu)。這些特點(diǎn)實(shí)際上是一些基礎(chǔ)的領(lǐng)域知識(shí)，假如為正確且準(zhǔn)確的描述這些特點(diǎn)設(shè)計(jì)一種恰當(dāng)?shù)臋C(jī)制，那么領(lǐng)域?qū)＜铱梢苑奖愕貐⑴c到需求建模過程中。本文通過定義需求模板來指導(dǎo)建立需求規(guī)約。需求模板如圖2 所示。所有的領(lǐng)域特點(diǎn)都被組織為模板中的節(jié)點(diǎn)和關(guān)鍵字，如系統(tǒng)需求可以被描述為功能函數(shù)、數(shù)據(jù)字典和不變量，每個(gè)函數(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ù)資源。特別是對(duì)于嵌入式控制軟件來說，在構(gòu)建非形式化需求規(guī)約階段，力求充分地將系統(tǒng)需要的全局變量等數(shù)據(jù)資源予以描述，對(duì)后續(xù)工作有重要指引作用。

大多數(shù)使用基于模型方法開發(fā)的軟件，其開發(fā)起點(diǎn)都是需求的獲取和分析。在需求規(guī)約建立初期，用戶需求通常是粗糙且不完整的，在這個(gè)階段，領(lǐng)域?qū)＜液蛙浖こ處熤g頻繁的交流非常重要，因此，在撰寫規(guī)約時(shí)使用自然語言更合適。非形式化需求文檔的構(gòu)建是一個(gè)初步建立需求描述的過程，在此過程中，需求內(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ī)約主要思想是對(duì)數(shù)據(jù)結(jié)構(gòu)或系統(tǒng)結(jié)構(gòu)等易于形式化定義的系統(tǒng)特征進(jìn)行精確描述，而將功能的輸出與輸出變量之間的關(guān)系或者軟件時(shí)序行為等難以直接用形式化語言描述的特征仍以自然語言描述。這樣的需求文檔可視為形式化和非形式化需求描述方式的一種平衡：既便于程序開發(fā)者理解需求，又便于需求分析者檢查文檔。

半形式化的需求文檔側(cè)重于對(duì)數(shù)據(jù)結(jié)構(gòu)的形式化定義。在多數(shù)嵌入式控制軟件中，存在大量全局變量，需要在需求分析和系統(tǒng)設(shè)計(jì)早期予以明確。需求分析人員需要形式化定義需求規(guī)約中涉及的所有數(shù)據(jù)結(jié)構(gòu)，并精確定義每個(gè)需求條目的輸入輸出變量，最后將需求重新定義為獨(dú)立函數(shù)。此時(shí)，需求規(guī)約是一個(gè)包含準(zhǔn)確接口定義的結(jié)構(gòu)化文件，但每個(gè)函數(shù)的前置、后置條件仍然是非形式化的。這一過程基于對(duì)領(lǐng)域知識(shí)和需求的理解，因?yàn)槊鞔_非形式化需求實(shí)際上是一個(gè)腦力工作，它依賴于對(duì)目標(biāo)系統(tǒng)中預(yù)期功能的理解。圖4 為上述非形式化規(guī)約對(duì)應(yīng)的半形式化規(guī)約。其中，編號(hào)為［SWRQ-0200］的需求被分解為多個(gè)函數(shù)，每個(gè)函數(shù)都準(zhǔn)確地定義了輸入輸出變量，但它們的前置、后置條件仍然是非形式化的。例如，變量MoOvEsState 是一個(gè)枚舉類型變量，WhMaSp 是一個(gè)速度單元，被定義在數(shù)據(jù)字典中。半形式化規(guī)約是一個(gè)結(jié)構(gòu)化的需求規(guī)約，它兼顧了準(zhǔn)確性和易讀性，可以方便地進(jìn)行快速審查和簡(jiǎn)單驗(yà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ī)約。這個(gè)形式化表示法和Python 語言的風(fēng)格類似，領(lǐng)域?qū)＜液蛙浖こ處煻伎梢院芸煺莆账D5 為形式化規(guī)約示例。

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

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

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

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

本文使用ANTLR（Another Tool for Language Recognition）作為實(shí)現(xiàn)解析器的組件。根據(jù)給定的語法信息，ANTLR 可以生成解析器解析生成AST，并返回詞法、語法信息。模型生成器使用深度優(yōu)先遍歷的方法遍歷AST 的每個(gè)葉子節(jié)點(diǎn)，生成需求模型。需求模型等價(jià)于形式化規(guī)約，但它更適用于機(jī)器讀取。通過分析需求模型，可以生成多個(gè)圖表以便驗(yàn)證需求正確性。算法1 解釋了如何從需求模型中自動(dòng)導(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)和驗(yàn)證

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

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

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

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

圖6 場(chǎng)景示例Fig.6 Example of scenario

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

表1 場(chǎng)景動(dòng)作Tabel 1 Scenario action

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

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

3.2 場(chǎng)景優(yōu)化

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

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

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

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

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

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

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

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

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

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

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

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

3.2.2 效率優(yōu)化

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

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

圖8 自動(dòng)生成場(chǎng)景流程Fig.8 Flow chart of automatically scenario generation

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

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

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

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

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

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

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

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

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

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

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

4 實(shí)驗(yàn)與結(jié)果分析

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

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

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

表4 實(shí)驗(yàn)結(jié)果比較Table 4 Comparsion of experimental result

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

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

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

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

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

圖10 測(cè)試用例示例Fig.10 Example of test case

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

5 結(jié)束語

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