發(fā)布者:凱思軟件發(fā)布日期:2023-09-05瀏覽量:
仿真已經成為大多數行業(yè)大規(guī)模采用基于模型的系統(tǒng)工程(MBSE)和基于模型的設計(MBD)工具的至關重要的因素。與此同時,實用的需求工程工具在以文檔需求規(guī)格為主的生命周期管理之外并未得到顯著發(fā)展,這使得需求并未得益于基于模型的仿真工具。需求在環(huán)(RIL)仿真已被提議用來擴展MBSE和MBD框架,允許系統(tǒng)工程師用一種正式的語言來描述文本需求,并且可以與系統(tǒng)模型一起執(zhí)行和仿真。需求在環(huán)仿真可允許基于需求語義生成離散時間系統(tǒng)行為,以及檢查狀態(tài)機等其他行為模型是否符合相關的系統(tǒng)需求。本文介紹了需求在環(huán)仿真的原則,并通過起落架系統(tǒng)案例講述了其所具備的優(yōu)勢。這項工作尤其彰顯了STIMULUS工具所具備的強大實力,包括檢測現(xiàn)實系統(tǒng)中錯誤的,缺失的或沖突的需求,以及測試其基于模型的需求規(guī)格是否符合相關需求。
引言
來自汽車、鐵路、航空電子、國防、航天、能源或醫(yī)療等關鍵安全領域的所有行業(yè)標準,都將需求置于開發(fā)和驗證流程的核心,其中需求工程工具通常用來管理以文檔為主的需求規(guī)格的生命周期。為了克服純文本需求規(guī)格在處理系統(tǒng)日益增加的復雜性方面的限制,我們推出了基于模型的系統(tǒng)工程(MBSE)[1]和基于模型的設計(MBD)[2]工具,并在大多數行業(yè)中進行了大規(guī)模的采用。仿真顯然是成功實現(xiàn)上述需求的關鍵因素,因為其為早期分析和驗證打開了機遇之門。
然而,基于模型的系統(tǒng)工程和需求工程工具之間的耦合仍然十分微弱。當前的行業(yè)實踐通常僅限于需求和模型之間的可追溯性流程。從仿真的角度來看,需求的執(zhí)行語義基本上還尚未得到利用,盡管我們已在這個領域開展了一系列的研究工作[3]。
需求在環(huán)仿真[4]旨在將實時功能需求轉變?yōu)樾问交模匀皇俏谋镜模蓤?zhí)行的模型。這些模型可以作為更大模型的一部分進行整合,通常是作為原理圖捕獲的系統(tǒng)架構,并與其他行為模型協(xié)同仿真。執(zhí)行引擎依賴于約束求解技術來生成離散時間仿真,其中我們通常將需求解讀為信號上的約束。
需要值得注意的是,需求和其他行為模型通常攜帶互補信息,因為它們捕獲了不同的抽象級別。舉例來說,安全需求可能會指定系統(tǒng)應該做什么,例如,在給定的延遲內對環(huán)境中的某些STIMULUS做出反應。因此,需求通常是部分的且非確定性的。相比之下,傳統(tǒng)的行為模型,如狀態(tài)機等,可能會更專注于如何進行反應,從而以更確定性的方式確保這種反應延遲。
需求在環(huán)仿真的應用包括兩個方面。一方面,形式化需求可以作為系統(tǒng)的許多不同行為的生成器,以調試和驗證在開發(fā)流程的早期階段的"內容"。另一方面,一旦模型可用,無論是詳細的需求規(guī)格還是實現(xiàn)模型,相關需求都可以作為觀察者用來開展測試和驗證的"方法"與"工具"。
在本文中,我們介紹了需求在環(huán)仿真的基本要素,并且我們在起落架客戶案例[5]中闡述了它的使用,該案例提供了一個具有代表性大小和復雜性的現(xiàn)實系統(tǒng)。我們展示了識別錯誤的,缺失的和沖突的需求以及驗證可執(zhí)行模型與其需求的能力。由于起落架的需求規(guī)格同時使用了文本需求,狀態(tài)機以及原理圖的混合信息,因此我們利用STIMULUS工具捕獲了完整的需求規(guī)格,并探討了其與第三方工具(如需求管理,MBSE或MBD工具等)的集成。
需求在環(huán)的基本要素
需求在環(huán)仿真致力于解決動態(tài)系統(tǒng)的功能需求。起落架客戶案例中的一個典型示例是以下的高級需求:“當操作桿命令為放時,所有起落架均應在15秒內完全展開,并且所有艙門應關閉?!?/strong>此類需求通常描述了系統(tǒng)隨時間變化的邏輯和數值屬性的組合。它們與非功能需求(如可用性或可靠性等)形成鮮明對比,后者并不受需求在環(huán)支持。
建模功能需求
進行需求在環(huán)仿真的前提是能夠捕獲此類需求的精確語義。為此,STIMULUS提供了一套預定義的句子模板,可以自由組合以構建文本需求,如圖1所示。句子模板可支持多種語言版本,用戶可以擴展預定義模板集以適應特定領域的需求。
圖1. 使用模板需求規(guī)格化的起落架系統(tǒng)需求
模板參數既可以參考標量表達式也可以參考語句,例如,“當......時”模板的條件和<主體>參數。每個模板的語義都通過等式和/或狀態(tài)機進行形式化定義。例如,“是”模板定義了多態(tài)的數學等式,而“當......時”模板定義了狀態(tài)機,當條件為真時,激活<主體>語句,如圖2所示。
圖2. “當......時”模板的語義
仿真需求
執(zhí)行需求的形式化語義的能力是需求在環(huán)仿真面臨的主要挑戰(zhàn)。STIMULUS的執(zhí)行引擎源于Lutin[6],這是一種原創(chuàng)語言,其完美結合了約束和正則表達式,以指定通用測試場景,以及Lurette[7],這是一種執(zhí)行引擎,可以從Lutin模型自動生成許多測試向量。此外,作者還指出了在需求工程中使用此類工具的巨大優(yōu)勢[12]。
STIMULUS按如下方式將這些原則擴展到了相關需求中:
需求規(guī)格語言對約束和狀態(tài)機進行了完美結合,采用了模式自動機[8]的同步語義,以正確處理分層和并行組合;
編譯器將一組采用這種語言進行表達的需求轉化為一組有時鐘的約束,遵循Lucid Synchron[9]的原始轉化模式;
模擬器將時鐘解譯為一個控制結構,以收集每個控制點[4]處的活動約束集,這可能會在執(zhí)行每個(離散時間)步驟時有所變化;
求解器計算活動約束的可能解空間,這是一組強耦合的布爾、數值和時間方程[10]的集合,并選擇其中一個解來計算系統(tǒng)輸出;
調試器允許檢查信號值、活動需求的亮點,以及改編自[11]的高級探索特性,以解釋為什么信號在精確的時間點有給定的值。
在此背景下,仿真意味著生成滿足需求約束的執(zhí)行追蹤,即可能的系統(tǒng)行為。由于需求規(guī)格本質上通常是部分的,因此并非確定性的,這樣的行為并非唯一。運行多次仿真將產生多種不同的行為,這對于測試自動化至關重要,相關內容將在第4節(jié)中進行深入探討。
圖3顯示了圖1中由STIMULUS生成的高級需求可能的執(zhí)行追蹤。由于我們并未指定起落架的伸出序列,艙門和起落架可能會經歷不同的狀態(tài)(定義為枚舉類型),但一旦HandleCommand輸入切換為放,艙門和起落架在預期的延遲內達到他們預期的狀態(tài)(分別為關閉和展開)。
本文的一個主要目標是展示如何將這個高級需求細化為更低級別的需求,這些需求將指定起落架收回和伸出序列的詳細信息。
圖3. 圖1中需求的可能的執(zhí)行追蹤
調試需求
盡管需求的聲明性質可提供如原子性、可組合性或可測試性等的眾多優(yōu)勢,但是,聲明性語言通常更難以進行調試。由于找出bug的原因比修復它需要花費時間更長,因此STIMULUS提供了多種調試功能來探索仿真的空間和時間維度。
標準的調試功能已根據相關需求進行了適應,比如高亮顯示活動/非活動需求,或者在任何時間點監(jiān)控任何變量。此外,許多原創(chuàng)功能專門針對需求的聲明性質給出了解決方案,以支持檢測三種類型的錯誤:
錯誤的需求(正確性):仿真運行良好,但仿真圖并未顯示預期的行為,這意味著一個或多個需求并未傳達出架構師的真正意圖。在這種情況下,高級探索功能有助于在任何時間點從任何變量中找出所涉及的需求。
缺失的需求(完整性):仿真運行良好,但部分仿真圖包含了虛線,意味著在這些時間段內,沒有活動的需求對它們進行定義。這可能是為了留下一些自由度以進行實施選擇,或者可能是缺失需求的跡象。
沖突的需求(一致性):仿真在某個時間點停止,意味著其中有一組需求是存在矛盾的,也就是說,一組約束沒有解。在這種情況下,求解器可自動報告沖突需求的最小集合。
其他建模方面
一些其他建模特性提高了形式化需求規(guī)格的一致性,以及它們在第三方工具中的集成。
原理圖語言可允許定義系統(tǒng)架構,這與任何MBSE或MBD工具類似。系統(tǒng)定義接口(輸入、輸出、參數)和行為,既可以是原理圖,也可以是需求和狀態(tài)機的組合,或者是外部的FMI組件。原理圖可以從其他工具導入,而形式化的需求可以與需求管理工具同步。
術語表允許定義可以在不同組件之間進行分享的系統(tǒng)變量。對于每個變量,術語表可選地指定數據類型、物理單位和/或物理維度、數值范圍或某些默認行為。類型系統(tǒng)支持推斷和多態(tài)性,這對于構建通用庫,以及在不提供任何類型信息的情況下檢查需求的一致性都是非常實用的。
需求在環(huán)仿真對起落架需求的處理
起落架系統(tǒng)[5]旨在根據航空器駕駛員的指令,控制三個起落架的伸出和收回序列。其主要由三部分組成。航空駕駛員界面提供了一個操縱裝置來指揮起落架的位置,以及作為顯示機械狀態(tài)的顯示器。數字部分負責將航空器駕駛員的指令轉化為電子命令,傳遞給物理部分。物理部分由三套起落設備組成,包括起落架、艙門,以及一些如電磁閥、模擬開關、液壓缸,以及用于捕獲機械狀態(tài)的傳感器等的電機設備。
圖4. 起落架系統(tǒng)架構
圖4的原理圖介紹了航空器駕駛員、數字部分和物理部分之間的交互??紤]到安全原因,數字部分是一個冗余系統(tǒng),其運行兩個實例的相同計算模塊。這個模塊包括伸出和收回序列的控制器,以及負責識別和消除無效傳感器的健康監(jiān)控系統(tǒng)。
整個架構在STIMULUS中以層次化的原理圖進行指定。術語表定義了所有的連接/接口信號,并且結構類型允許信號的復用,例如,DoorsClosedSensors是一個3x3的布爾矩陣,用于捕獲每個起落架套裝的三重傳感器。
形式化的需求可以分配給系統(tǒng)架構的任何級別。例如,圖1的高級需求分配給了數字部分,并且詳細的細化需求可以分配給基礎組件,如控制器和物理設備等。
物理部分的需求
原始需求規(guī)格以自由文本的形式介紹了物理設備的行為。對于每臺設備,此行為已經被捕獲為一組形式化的需求,在此可以單獨進行仿真。例如,模擬開關的自由文本描述如圖5所示。
“每次航空器駕駛員移動操縱桿時,開關都會關閉,并保持關閉20秒。此時長過后,開關會自動變?yōu)榇蜷_狀態(tài)。在閉合位置時,開關將數字部分的電氣指令傳輸給通用電磁閥。在打開位置,電氣指令沒有被發(fā)送到電磁閥。由于慣性原因,從兩種狀態(tài)進行轉換需要一定的時間:從打開到閉合需要0.8秒,從閉合到打開需要1.2秒?!?
圖5. 模擬開關非形式化需求規(guī)格
圖6. 模擬開關的形式化需求
圖6給出了模擬開關的形式化需求,而圖7顯示了一個可能的仿真。HandleMove信號的行為受到約束,以發(fā)出隨機脈沖,而輸入信號是具有隨機值的自由變量。每次發(fā)出HandleMove信號時,開關都會關閉,輸入信號會傳輸到輸出信號。
然而,對仿真圖進行深入觀察會發(fā)現(xiàn)一個錯誤的行為,因為在t=50s時的HandleMove脈沖應該將開關保持在關閉狀態(tài),直至t=70s。將第二個需求的條件替換為“狀態(tài)變?yōu)殛P閉或HandleMove變?yōu)檎妗笨梢越鉀Q這個問題。
圖7. 可能的模擬開關需求的仿真結果
數字部分的需求
原始的伸出序列需求規(guī)格在圖8中給出。其本身并不是一組需求,而是一個標準的情景,因為其描述了在完成一個完整的伸出序列過程中,數字控制器發(fā)送的命令序列以及物理部分的反應。此外,附注特別說明,這個標準的序列可以在任何時候被反向命令打斷,而且這個序列會在被打斷的地方恢復。
盡管這個需求規(guī)格非常全面,但其并沒有提供統(tǒng)一且可測試的需求來描述系統(tǒng)在任何時間點應執(zhí)行的操作。深入分析此類需求是一個非常艱難的過程,并沒有什么神奇的簡單方法:我們是通過不斷地試驗、錯誤和修正進行的。然而,事實證明,仿真在檢測連續(xù)的錯誤和向圖9中的形式化需求集合進展的過程中是至關重要的。
伸出序列。起落架的伸出可分解為一系列基本動作。當起落架鎖定于收起位置,且艙門鎖定于關閉位置時,若航空器駕駛員將操縱桿設置為“放”,則軟件應產生以下一系列動作。
激勵常規(guī)電磁閥將指令單元分離,從而向作動電磁閥傳遞液壓力。
激勵艙門開啟電磁閥。
當三個艙門均抵達開啟位置時,激勵起落架釋放電磁閥。
當三個起落架被鎖定,停止激勵起落架釋放電磁閥。
停止激勵艙門開啟電磁閥。
激勵艙門關閉電磁閥。
當三個艙門均抵達關閉位置且鎖定,停止激勵艙門關閉電磁閥。
最終停止激勵常規(guī)電磁閥。
反向指令應隨時均對以上動作序列具有中斷效果(如釋放序列中遭遇收起指令和收起序列中遭遇釋放指令)。在此類情況下,有關場景由中斷處繼續(xù)執(zhí)行。
圖8. 傳出序列的非形式化需求規(guī)格
圖9. 伸出序列的形式化需求
需求仿真分析
一旦所有軟件和物理需求都已形式化并分配給系統(tǒng)架構中的適當組件,我們就可以仿真完整的系統(tǒng)行為。從建模的角度來看,這就是與現(xiàn)有的MBSE/MBD工具的連接發(fā)揮其全部作用的地方,因為系統(tǒng)架構通常可以根據相應的需求由STIMULUS導入。由于需求的分配被保留,系統(tǒng)架構師可以在他們的標準MBSE工具中對架構進行建模,并在非常早期的階段在STIMULUS中對其進行仿真,而無需等待更詳細的行為模型。
可能的仿真如圖10所示。HandleCommand信號首先從放切換到收,然后,在收回序列完成之前,切換回放,以激活伸出序列。我們可以看到,反指令得到了妥善的管理。收起序列一直運行到所有的艙門都打開,所有的起落架都在操縱以回收。然后啟動了伸出序列。由于所有的艙門都已經打開,伸出序列立即開始操縱以展開起落架,一旦展開起落架,就完成了相應的序列,關閉了艙門。
圖10. 可能的起落架需求仿真
圖1中的高級需求,作為數字部分的觀察者,也得到了滿足。換言之,伸出序列的詳細需求是對其的優(yōu)異細化。
然而,圖11中的第一個安全性需求在時間t=10.3s處遭到違反,因為數字部分向艙門發(fā)送了相互矛盾的指令。在一個時間點,物理系統(tǒng)被要求同時打開和關閉艙門。STIMULUS會自動報告這個沖突,并給出精確的診斷,從而識別出一組沖突的需求和沖突的瞬間。
圖11. 伸出和收回序列的安全需求
由于篇幅原因以及作者對游戲感的缺乏,讀者被邀請代入系統(tǒng)架構師的角色,提出一個詳細的修改需求以避免這種沖突的建議。在第二步中,讀者被邀請在不進行任何仿真測試的情況下,思考他們對這種改變抱有多大的信心。
針對需求進行模型測試
一旦驗證通過,形式化需求可以轉化為觀察者,用來測試任何模型的需求規(guī)格,或者起落架的軟硬件實現(xiàn)。對于硬件在環(huán)(Hardware-In-the-Loop)仿真,觀察者被導出為FMI組件以監(jiān)控測試工作臺并記錄違反的需求。對于模型或軟件在環(huán)(Model- or Software-In-the-Loop)仿真,F(xiàn)MI組件被從第三方MBSE/MBD工具導入STIMULUS,以構建測試套件并自動化回歸測試。
在這個客戶案例中,我們已經將一些數字和物理組件建模為狀態(tài)機,其中一些是由原始論文[5]提供的,以便根據需求測試需求規(guī)格模型。尤其是,我們返回到伸出序列的原始需求規(guī)格,因為人們可能認為,使用狀態(tài)機對這個序列及其中斷進行建模是非常直觀的。
圖12展示了STIMULUS的分層狀態(tài)機模型,其中包含一個恢復轉換(由空箭頭標示)。如預期的那樣,對于完整的伸出序列的名義場景,狀態(tài)機工作正常。然而,這個模型并未正確處理反向指令,許多需求觀察者在此類仿真中遭到違反。
與原始需求規(guī)格中的表述不同,序列不應該“從中斷的地方繼續(xù)”。實際上,恢復狀態(tài)依賴于艙門和起落架的物理狀態(tài),并且應該為序列的每個狀態(tài)都添加特定的傳入轉換。再次,我們讓讀者提出新的需求規(guī)格,并找出缺失的轉換條件。最后,我們還指出,一個明智的原理圖控制器實際上可以從形式化的需求中得出,并提供一個優(yōu)異的備選狀態(tài)機。
圖12. 伸出序列的初級狀態(tài)機需求規(guī)格
可執(zhí)行需求和模型的結合為基于模型的測試提供了一個良好的框架。特別是,形式化需求有助于設置一個測試線束來自動化回歸測試。在這項工作中:
我們將數字控制器視為被測系統(tǒng)(SUT)。其可以是一個模型,例如狀態(tài)機,或一個外部的FMI組件;
我們將航空器駕駛員視為測試案例。命令可以被建模為約束,以生成各種測試場景(常規(guī),反向命令);
我們將物理部分視為測試存根。其可以是需求和狀態(tài)機的結合,并對SUT環(huán)境進行仿真;
我們將數字控制器的需求視為測試預言,作為觀察者執(zhí)行。
我們的結果顯示了對初始起落架和艙門位置的廣泛探索,以及它們對伸出和收回序列執(zhí)行的影響,這些序列通??偸菨M足圖1的高級需求。
結論
本客戶案例展示了對需求在環(huán)仿真的使用,對調試和驗證具有實際復雜性的典型網絡物理系統(tǒng)功能需求規(guī)格的應用。
研究結果表明,需求在環(huán)(RIL)仿真非常適合基于模型的系統(tǒng)工程方法,因為可以以一種一體化和一致性的方式來設計需求、架構和行為模型。尤其是,可以將給定系統(tǒng)的需求細化為其子系統(tǒng)的更低級別需求,直至定義行為模型。在細化過程的任何步驟,都會進行仿真以檢查全局系統(tǒng)架構的一致性以及低級別需求和/或模型與高級別需求的合規(guī)性。
這提供了一個有效的基于模型的測試框架,其中需求輪流捕獲被測試系統(tǒng)、測試預言、測試用例或測試存根。測試執(zhí)行引擎充分利用約束求解技術來探索各種環(huán)境場景和被測試系統(tǒng)的可能反應,從而實現(xiàn)全自動回歸測試。盡管仿真無法確保探索的窮盡性,但其似乎是手動測試的有限覆蓋率和自動證明工具的有限采用率之間的有效權衡。
最后,這項研究的一個有趣結果涉及到故障分析。傳感器模型已經擴展了概率故障,通過仿真驗證健康監(jiān)控系統(tǒng)的需求。這一研究工作的初步成果非常鼓舞人心,為這一領域未來工作的開展打開了機遇之門。