進(jìn)行需求在環(huán)仿真的前提是能夠捕獲此類需求的精確語義。為此，STIMULUS提供了一套預(yù)定義的句子模板，可以自由組合以構(gòu)建文本需求，如圖1所示。句子模板可支持多種語言版本，用戶可以擴(kuò)展預(yù)定義模板集以適應(yīng)特定領(lǐng)域的需求。

圖1. 使用模板需求規(guī)格化的起落架系統(tǒng)需求

模板參數(shù)既可以參考標(biāo)量表達(dá)式也可以參考語句，例如，“當(dāng)......時(shí)”模板的條件和<主體>參數(shù)。每個(gè)模板的語義都通過等式和/或狀態(tài)機(jī)進(jìn)行形式化定義。例如，“是”模板定義了多態(tài)的數(shù)學(xué)等式，而“當(dāng)......時(shí)”模板定義了狀態(tài)機(jī)，當(dāng)條件為真時(shí)，激活<主體>語句，如圖2所示。

圖2. “當(dāng)......時(shí)”模板的語義

執(zhí)行需求的形式化語義的能力是需求在環(huán)仿真面臨的主要挑戰(zhàn)。STIMULUS的執(zhí)行引擎源于Lutin[6]，這是一種原創(chuàng)語言，其完美結(jié)合了約束和正則表達(dá)式，以指定通用測試場景，以及Lurette[7]，這是一種執(zhí)行引擎，可以從Lutin模型自動生成許多測試向量。此外，作者還指出了在需求工程中使用此類工具的巨大優(yōu)勢[12]。

在此背景下，仿真意味著生成滿足需求約束的執(zhí)行追蹤，即可能的系統(tǒng)行為。由于需求規(guī)格本質(zhì)上通常是部分的，因此并非確定性的，這樣的行為并非唯一。運(yùn)行多次仿真將產(chǎn)生多種不同的行為，這對于測試自動化至關(guān)重要，相關(guān)內(nèi)容將在第4節(jié)中進(jìn)行深入探討。

圖3顯示了圖1中由STIMULUS生成的高級需求可能的執(zhí)行追蹤。由于我們并未指定起落架的伸出序列，艙門和起落架可能會經(jīng)歷不同的狀態(tài)（定義為枚舉類型），但一旦HandleCommand輸入切換為放，艙門和起落架在預(yù)期的延遲內(nèi)達(dá)到他們預(yù)期的狀態(tài)（分別為關(guān)閉和展開）。

本文的一個(gè)主要目標(biāo)是展示如何將這個(gè)高級需求細(xì)化為更低級別的需求，這些需求將指定起落架收回和伸出序列的詳細(xì)信息。

圖3. 圖1中需求的可能的執(zhí)行追蹤

盡管需求的聲明性質(zhì)可提供如原子性、可組合性或可測試性等的眾多優(yōu)勢，但是，聲明性語言通常更難以進(jìn)行調(diào)試。由于找出bug的原因比修復(fù)它需要花費(fèi)時(shí)間更長，因此STIMULUS提供了多種調(diào)試功能來探索仿真的空間和時(shí)間維度。

一些其他建模特性提高了形式化需求規(guī)格的一致性，以及它們在第三方工具中的集成。

原理圖語言可允許定義系統(tǒng)架構(gòu)，這與任何MBSE或MBD工具類似。系統(tǒng)定義接口（輸入、輸出、參數(shù)）和行為，既可以是原理圖，也可以是需求和狀態(tài)機(jī)的組合，或者是外部的FMI組件。原理圖可以從其他工具導(dǎo)入，而形式化的需求可以與需求管理工具同步。

術(shù)語表允許定義可以在不同組件之間進(jìn)行分享的系統(tǒng)變量。對于每個(gè)變量，術(shù)語表可選地指定數(shù)據(jù)類型、物理單位和/或物理維度、數(shù)值范圍或某些默認(rèn)行為。類型系統(tǒng)支持推斷和多態(tài)性，這對于構(gòu)建通用庫，以及在不提供任何類型信息的情況下檢查需求的一致性都是非常實(shí)用的。

起落架系統(tǒng)[5]旨在根據(jù)航空器駕駛員的指令，控制三個(gè)起落架的伸出和收回序列。其主要由三部分組成。航空駕駛員界面提供了一個(gè)操縱裝置來指揮起落架的位置，以及作為顯示機(jī)械狀態(tài)的顯示器。數(shù)字部分負(fù)責(zé)將航空器駕駛員的指令轉(zhuǎn)化為電子命令，傳遞給物理部分。物理部分由三套起落設(shè)備組成，包括起落架、艙門，以及一些如電磁閥、模擬開關(guān)、液壓缸，以及用于捕獲機(jī)械狀態(tài)的傳感器等的電機(jī)設(shè)備。

圖4. 起落架系統(tǒng)架構(gòu)

圖4的原理圖介紹了航空器駕駛員、數(shù)字部分和物理部分之間的交互。考慮到安全原因，數(shù)字部分是一個(gè)冗余系統(tǒng)，其運(yùn)行兩個(gè)實(shí)例的相同計(jì)算模塊。這個(gè)模塊包括伸出和收回序列的控制器，以及負(fù)責(zé)識別和消除無效傳感器的健康監(jiān)控系統(tǒng)。

整個(gè)架構(gòu)在STIMULUS中以層次化的原理圖進(jìn)行指定。術(shù)語表定義了所有的連接/接口信號，并且結(jié)構(gòu)類型允許信號的復(fù)用，例如，DoorsClosedSensors是一個(gè)3x3的布爾矩陣，用于捕獲每個(gè)起落架套裝的三重傳感器。

形式化的需求可以分配給系統(tǒng)架構(gòu)的任何級別。例如，圖1的高級需求分配給了數(shù)字部分，并且詳細(xì)的細(xì)化需求可以分配給基礎(chǔ)組件，如控制器和物理設(shè)備等。

原始需求規(guī)格以自由文本的形式介紹了物理設(shè)備的行為。對于每臺設(shè)備，此行為已經(jīng)被捕獲為一組形式化的需求，在此可以單獨(dú)進(jìn)行仿真。例如，模擬開關(guān)的自由文本描述如圖5所示。

圖5. 模擬開關(guān)非形式化需求規(guī)格

圖6. 模擬開關(guān)的形式化需求

圖6給出了模擬開關(guān)的形式化需求，而圖7顯示了一個(gè)可能的仿真。HandleMove信號的行為受到約束，以發(fā)出隨機(jī)脈沖，而輸入信號是具有隨機(jī)值的自由變量。每次發(fā)出HandleMove信號時(shí)，開關(guān)都會關(guān)閉，輸入信號會傳輸?shù)捷敵鲂盘枴?

然而，對仿真圖進(jìn)行深入觀察會發(fā)現(xiàn)一個(gè)錯(cuò)誤的行為，因?yàn)樵趖=50s時(shí)的HandleMove脈沖應(yīng)該將開關(guān)保持在關(guān)閉狀態(tài)，直至t=70s。將第二個(gè)需求的條件替換為“狀態(tài)變?yōu)殛P(guān)閉或HandleMove變?yōu)檎妗笨梢越鉀Q這個(gè)問題。

圖7. 可能的模擬開關(guān)需求的仿真結(jié)果

原始的伸出序列需求規(guī)格在圖8中給出。其本身并不是一組需求，而是一個(gè)標(biāo)準(zhǔn)的情景，因?yàn)槠涿枋隽嗽谕瓿梢粋€(gè)完整的伸出序列過程中，數(shù)字控制器發(fā)送的命令序列以及物理部分的反應(yīng)。此外，附注特別說明，這個(gè)標(biāo)準(zhǔn)的序列可以在任何時(shí)候被反向命令打斷，而且這個(gè)序列會在被打斷的地方恢復(fù)。

盡管這個(gè)需求規(guī)格非常全面，但其并沒有提供統(tǒng)一且可測試的需求來描述系統(tǒng)在任何時(shí)間點(diǎn)應(yīng)執(zhí)行的操作。深入分析此類需求是一個(gè)非常艱難的過程，并沒有什么神奇的簡單方法：我們是通過不斷地試驗(yàn)、錯(cuò)誤和修正進(jìn)行的。然而，事實(shí)證明，仿真在檢測連續(xù)的錯(cuò)誤和向圖9中的形式化需求集合進(jìn)展的過程中是至關(guān)重要的。

圖8. 傳出序列的非形式化需求規(guī)格

圖9. 伸出序列的形式化需求

一旦所有軟件和物理需求都已形式化并分配給系統(tǒng)架構(gòu)中的適當(dāng)組件，我們就可以仿真完整的系統(tǒng)行為。從建模的角度來看，這就是與現(xiàn)有的MBSE/MBD工具的連接發(fā)揮其全部作用的地方，因?yàn)橄到y(tǒng)架構(gòu)通?？梢愿鶕?jù)相應(yīng)的需求由STIMULUS導(dǎo)入。由于需求的分配被保留，系統(tǒng)架構(gòu)師可以在他們的標(biāo)準(zhǔn)MBSE工具中對架構(gòu)進(jìn)行建模，并在非常早期的階段在STIMULUS中對其進(jìn)行仿真，而無需等待更詳細(xì)的行為模型。

可能的仿真如圖10所示。HandleCommand信號首先從放切換到收，然后，在收回序列完成之前，切換回放，以激活伸出序列。我們可以看到，反指令得到了妥善的管理。收起序列一直運(yùn)行到所有的艙門都打開，所有的起落架都在操縱以回收。然后啟動了伸出序列。由于所有的艙門都已經(jīng)打開，伸出序列立即開始操縱以展開起落架，一旦展開起落架，就完成了相應(yīng)的序列，關(guān)閉了艙門。

圖10. 可能的起落架需求仿真

圖1中的高級需求，作為數(shù)字部分的觀察者，也得到了滿足。換言之，伸出序列的詳細(xì)需求是對其的優(yōu)異細(xì)化。

然而，圖11中的第一個(gè)安全性需求在時(shí)間t=10.3s處遭到違反，因?yàn)閿?shù)字部分向艙門發(fā)送了相互矛盾的指令。在一個(gè)時(shí)間點(diǎn)，物理系統(tǒng)被要求同時(shí)打開和關(guān)閉艙門。STIMULUS會自動報(bào)告這個(gè)沖突，并給出精確的診斷，從而識別出一組沖突的需求和沖突的瞬間。

圖11. 伸出和收回序列的安全需求

由于篇幅原因以及作者對游戲感的缺乏，讀者被邀請代入系統(tǒng)架構(gòu)師的角色，提出一個(gè)詳細(xì)的修改需求以避免這種沖突的建議。在第二步中，讀者被邀請?jiān)诓贿M(jìn)行任何仿真測試的情況下，思考他們對這種改變抱有多大的信心。

一旦驗(yàn)證通過，形式化需求可以轉(zhuǎn)化為觀察者，用來測試任何模型的需求規(guī)格，或者起落架的軟硬件實(shí)現(xiàn)。對于硬件在環(huán)（Hardware-In-the-Loop）仿真，觀察者被導(dǎo)出為FMI組件以監(jiān)控測試工作臺并記錄違反的需求。對于模型或軟件在環(huán)（Model- or Software-In-the-Loop）仿真，F(xiàn)MI組件被從第三方MBSE/MBD工具導(dǎo)入STIMULUS，以構(gòu)建測試套件并自動化回歸測試。

在這個(gè)客戶案例中，我們已經(jīng)將一些數(shù)字和物理組件建模為狀態(tài)機(jī)，其中一些是由原始論文[5]提供的，以便根據(jù)需求測試需求規(guī)格模型。尤其是，我們返回到伸出序列的原始需求規(guī)格，因?yàn)槿藗兛赡苷J(rèn)為，使用狀態(tài)機(jī)對這個(gè)序列及其中斷進(jìn)行建模是非常直觀的。

圖12展示了STIMULUS的分層狀態(tài)機(jī)模型，其中包含一個(gè)恢復(fù)轉(zhuǎn)換（由空箭頭標(biāo)示）。如預(yù)期的那樣，對于完整的伸出序列的名義場景，狀態(tài)機(jī)工作正常。然而，這個(gè)模型并未正確處理反向指令，許多需求觀察者在此類仿真中遭到違反。

與原始需求規(guī)格中的表述不同，序列不應(yīng)該“從中斷的地方繼續(xù)”。實(shí)際上，恢復(fù)狀態(tài)依賴于艙門和起落架的物理狀態(tài)，并且應(yīng)該為序列的每個(gè)狀態(tài)都添加特定的傳入轉(zhuǎn)換。再次，我們讓讀者提出新的需求規(guī)格，并找出缺失的轉(zhuǎn)換條件。最后，我們還指出，一個(gè)明智的原理圖控制器實(shí)際上可以從形式化的需求中得出，并提供一個(gè)優(yōu)異的備選狀態(tài)機(jī)。

圖12. 伸出序列的初級狀態(tài)機(jī)需求規(guī)格

我們的結(jié)果顯示了對初始起落架和艙門位置的廣泛探索，以及它們對伸出和收回序列執(zhí)行的影響，這些序列通常總是滿足圖1的高級需求。

本客戶案例展示了對需求在環(huán)仿真的使用，對調(diào)試和驗(yàn)證具有實(shí)際復(fù)雜性的典型網(wǎng)絡(luò)物理系統(tǒng)功能需求規(guī)格的應(yīng)用。

研究結(jié)果表明，需求在環(huán)（RIL）仿真非常適合基于模型的系統(tǒng)工程方法，因?yàn)榭梢砸砸环N一體化和一致性的方式來設(shè)計(jì)需求、架構(gòu)和行為模型。尤其是，可以將給定系統(tǒng)的需求細(xì)化為其子系統(tǒng)的更低級別需求，直至定義行為模型。在細(xì)化過程的任何步驟，都會進(jìn)行仿真以檢查全局系統(tǒng)架構(gòu)的一致性以及低級別需求和/或模型與高級別需求的合規(guī)性。

這提供了一個(gè)有效的基于模型的測試框架，其中需求輪流捕獲被測試系統(tǒng)、測試預(yù)言、測試用例或測試存根。測試執(zhí)行引擎充分利用約束求解技術(shù)來探索各種環(huán)境場景和被測試系統(tǒng)的可能反應(yīng)，從而實(shí)現(xiàn)全自動回歸測試。盡管仿真無法確保探索的窮盡性，但其似乎是手動測試的有限覆蓋率和自動證明工具的有限采用率之間的有效權(quán)衡。

最后，這項(xiàng)研究的一個(gè)有趣結(jié)果涉及到故障分析。傳感器模型已經(jīng)擴(kuò)展了概率故障，通過仿真驗(yàn)證健康監(jiān)控系統(tǒng)的需求。這一研究工作的初步成果非常鼓舞人心，為這一領(lǐng)域未來工作的開展打開了機(jī)遇之門。