LTS仿真模型組合驗證方法

馮曉寧, 王卓, 王金娜

(1.哈爾濱工程大學 計算機科學與技術學院，黑龍江 哈爾濱 150001；2.哈爾濱工程大學 船舶工程學院，黑龍江 哈爾濱 150001)

為提高復雜仿真系統的開發效率和降低開發成本，將仿真模型進行重用是當前最有效的解決方法之一。但如何重用已有的仿真模型從而實現仿真系統的快速構造，即仿真模型的可組合問題已經成為該領域所面臨的重大挑戰。而仿真模型組合需要解決的一個重要問題就是組合后的仿真模型是否滿足用戶需求，是否為有效仿真模型，即仿真模型組合的驗證問題。Petty等提出了語義可組合理論(semantic composability theory，SCT)[1-3]。SCT中給出了完美模型(或稱請求模型)的定義。認為完美模型是一個概念模型，它的初始狀態和輸入與自然系統中的模型行為完全一致，并且一個反映真實系統的模型應該具有與真實系統相似的行為。我國的王維平等在Petty等的基礎上，根據不同領域仿真模型的組合和重用需求，對仿真模型可組合問題進行了系統的研究[4-7]。基于此，本文提出一種基于LTS的仿真模型組合驗證方法。該方法在仿真模型的行為表示中引入了時間因素，并將模型的執行序列表示為LTS。通過比較二者的LTS來驗證組合仿真模型的行為，從而得出組合仿真模型是否有效。

1 模型組合驗證方法

對于一個給定的初始條件和一組輸入值，一個仿真模型表現出來的行為應該與請求模型的行為非常接近。依此想法，驗證組合仿真模型的有效性則是基于判斷行為匹配的相近程度。

該驗證方法主要分為4個步驟：1)行為展開；2)行為組合；3)模型行為表示為LTS；4)仿真模型的有效性驗證，如圖1所示。前3個步驟都分別在組合仿真模型與請求模型上獨立執行，第4個步驟為組合仿真模型與請求模型共同參與。本文將對步驟1)～3)進行詳細說明。

圖1 仿真模型組合的驗證過程

仿真模型在開發完成后，開發者給出一個仿真模型的概念描述，稱為元模型，元模型描述仿真模型的屬性和行為，并應用于仿真模型發現以及驗證框架中。元模型以一個狀態機的形式表示仿真模型的行為，表示為

(1)

式中：I表示輸入數據集合，Sp是當前狀態，Δt是狀態轉換的時間間隔，狀態轉換需要滿足一定的條件Cond，St是轉換后的狀態，O是狀態轉換后的輸出數據集合，Am是狀態轉換后改變的性質的集合。為了避免狀態爆炸，每個仿真模型都只考慮影響狀態轉換的通信狀態和屬性。

驗證方法的步驟1行為展開過程基于仿真模型的執行時間，本文將狀態機表示的概念仿真模型行為進行統一規范化表示為

(2)

式中：fi代表仿真模型Mi的形式化表示，表達式中t為狀態開始轉換的時刻，經過Δt的轉換時間間隔，t+Δt為狀態轉換后的時刻。

仿真行為展開的過程就是將每個仿真模型按任務執行數τ以及平均執行時間Δt展開，得到表示仿真模型執行行為表達式的全過程。展開需要依據2個因素：任務執行數τ和仿真模型的平均執行時間Δt。

驗證方法步驟2)，仿真模型行為組合主要考慮以下約束規則：任意相互組合的2個仿真模型，后者需求輸入的時間必須大于等于前者產生輸出的時間；“連接件的傳輸時間”必須考慮，它是一個概念上的名詞，表示相互組合的2個仿真模型數據從一方傳輸到另一方的時間延遲；同一個基礎仿真模型，執行第2個任務的開始時間必須大于等于前一個任務的結束時間。

步驟3)為將仿真模型的執行序列表示為LTS。起始時刻從0開始，根據組合時間約束，得出組合仿真模型M的任務交錯執行序列。將該序列表示為一個標簽轉移系統L(M):

(3)

式中：N表示節點的集合，Act表示轉換標簽的集合，→表示節點間轉換的集合。

N中的每個節點都表示一個帶有注釋的組合狀態，該組合狀態是一個三元組:

(4)

式中：state(fi)是仿真模型fi的狀態，fin是經過LTS進入該節點的仿真模型，fout是經過LTS離開該節點的仿真模型。Act集合中的每一個標簽也是一個三元組:

(5)

三元組中的name(fout)指經過LTS離開該節點的仿真模型名稱，duration(fout)表示經過LTS離開該節點的仿真模型的執行時間間隔，output(fout)是該仿真模型的輸出，即經過LTS進入該節點或者離開該節點的仿真模型名稱。一個組合仿真模型M的仿真行為序列和與它對應的標簽轉移系統L(M)如圖2所示。

圖2 模型執行序列和對應的LTS

2 模型組合有效性驗證

本文將仿真模型的行為序列表示為LTS，比較組合仿真模型的行為與請求模型的行為，可以通過比較二者LTS之間的關系得出。若二者的LTS強等價，則證明組合仿真模型有效。

L(MR)=(NR,Act,→)，L(M)=(N,Act,→)

分別為請求模型行為序列與組合仿真模型行為序列的標簽轉移系統。

定義1 仿真模型強模擬

定義2 仿真模型強等價

關系R?NR×N是仿真模型強等價，當且僅當對于所有的(nR,n)∈R,σ∈Act：

稱M與MR存在仿真模型強等價關系，也稱為仿真模型強互模擬，表示為L(M)?RL(MR)。其中nR和n分別表示請求模型和組合仿真模型執行行為序列的帶注釋三元組組合狀態。

組合仿真模型與請求模型的執行行為序列LTS之間的強等價關系驗證過程可用CADP[8]工具中的BISIMULATOR互模擬工具自動驗證。

在現實中，2個仿真模型剛好存在強等價的情況非常少，大部分足夠接近請求模型。當表示組合仿真模型與請求模型的執行序列的LTS不存在強等價關系時，如何判斷組合仿真模型有效，是一個需要解決的問題。為此，作者提出了語義相似度關系Vε，比較2個仿真模型行為序列對應的LTS的節點的語義信息，根據LTS的節點語義信息計算語義相似度距離，若該語義相似度距離小于ε，則兩個LTS存在帶有參數ε的弱等價關系Vε，并且組合模型為語義有效模型。

定義3 語義相似度關系Vε,令組合仿真模型的LTS表示為L(M)= (P,Act，→)請求模型的LTS表示為L(MR)= (Q,Act,→) ，P和Q分別是L(M)和L(MR)中帶注釋的狀態集合，集合中的每個元素都是一個三元組，且任意p∈P,q∈Q可表示為

(6)

s(p)和sR(q)代表仿真模型的狀態。

(7)

則語義相似度關系：

(8)

(9)

式中：DS(s(p),sR(q))是組合狀態間的語義距離,DF(fi,fjR)是仿真模型函數名之間的語義函數距離。

語義狀態距離用于度量仿真模型屬性間的語義距離，計算方法為：令s(p)與sR(q)的狀態滿足式(7)，則p與q的語義狀態距離DS(s(p),sR(q))為

(10)

其中,ds(state(fi),state(fiR)的計算方法為：

(11)

式中：A(fi)是仿真模型fi的屬性集合，m= |A(fi)|且d(ai,ajR)的定義為：

(12)

式中：(ai,ajR)相關是指在組件的建模與仿真本體(component simulation and modeling ontology,COSMO)中相關[9-10]。語義相似度關系Vε主要考慮COSMO本體的組合狀態間關系，它以仿真模型屬性為依據。

語義函數距離用于確定進入和離開LTS的函數是否相關。假設fi(p)、fjR(q)分別是標簽轉移系統L(M)和L(MR)中對應的進入或離開節點p和q的函數，則語義函數距離DF(fi(p)、fjR(q))為：

(13)

3 仿真模型組合實例驗證

仿真模型的驗證過程通常是冗長的并且是手工完成的，需要系統專家在場。特別是當仿真模型用在關鍵場景中(如軍事作戰)，驗證模型的有效性就顯得至關重要。本文使用軍事作戰坦克修理所模型作為應用實例，針對仿真模型組合的動態驗證方法進行詳細說明。

3.1 作戰坦克修理所

現代化軍事作戰仿真場景中，部隊的坦克經過作戰以后若出現較大的故障，通常要進入坦克修理所進行修理。坦克修理所工作流程圖如圖3所示。假設該修理所一次只能修理一輛坦克，且故障坦克到達修理所的時間間隔與修理坦克所花費的時間間隔都是隨機的，服從指數分布。故障坦克的維修方式是先到的先進行維修，這是一個典型的單服務隊列排隊系統。

通過仿真模型發現，在軍事作戰仿真系統開發模型庫中找到類似功能的重用單服務隊列模型。該仿真模型由3個基礎仿真模型組成，分別為M1、M2和M3。其中M1負責接收請求并按先后到達的時間順序進行排隊，M2對接收到的請求按排隊順序進行服務，M3將服務完成的結果進行輸出。M1、M2和M3都有一個對應的元模型描述，具體內容見表1。其中M1請求抵達的時間服從指數分布且平均抵達時間為3。M2服務一個請求的時間也服從指數分布且平均服務時間為6。M3的平均打印輸出時間為1。這里的時間3、6和1指的不是具體的時分秒時間，而是代表是時間單位。

圖3 坦克修理所工作流程圖

表1 組合仿真模型的元模型描述

3.2 坦克修理所模型展開

根據表1中的狀態機信息，可將仿真模型M1、M2和M3的行為規范化表示為以下形式：

將M1、M2、M3分別按τ=4次和平均執行時間展開。狀態S的下標表示所屬的仿真模型，例如S1表示該狀態屬于M1。狀態S的次下標表示該仿真模型中的第幾個狀態，例如S12表示M1中的第2個狀態，S23表示M2中的第3個狀態。

則M1展開式如下：

M2展開式為

M3展開式為：

根據連接件屬性，假設M1與M24次傳輸數據在連接件上的耗費時間為Δw1=3; Δw2=2; Δw3= 1; Δw4= 1,并且M2與M34次傳輸數據在連接件上的耗費時間為Δw1'=4;Δw2'=3;Δw3'= 2; Δw4'= 2。由仿真模型組合主要考慮的3點時間約束規則，得出x、y、z、r和x'、y'、z'、r'的時間約束如下：

得到一組滿足組合仿真模型執行行為的時間解：x=6,y=12,z=18,r=24,x'=16,y'=21,z'=26,r'=32。

請求模型按照以上方式展開,最終得到滿足請求模型組合條件的時間解為：xR=6,yR=14,zR=20,rR=25,x′R=18,y′R=23,z′R=27,r′R=32。

3.3 仿真過程及有效性驗證

根據上一步滿足時間條件的解，得出組合仿真模型與請求模型按時間交替執行的行為序列如下：

將執行序列表示為LTS，如圖4所示。圖形的上半部分L(M)為組合仿真模型的LTS，下半部分L(MR)為請求模型的LTS。

(a) 組合模型LTS

(b) 請求模型LTS

對L(M)和L(MR)進行比較，使用CADP中的BISIMULATOR檢測。通過狀態S3、S8、S10和S3R、S8R、S10R的輸出標簽，明顯可以得出L(M)與L(MR)之間不存在強等價關系，故BISIMULATOR工具的返回值為false。計算語義相似度關系Vε={(Si,SjR)‖i≠3, 8,10},故組合仿真模型M為語義有效模型。

4 結束語

本文針對仿真模型組合的驗證方法進行了研究，提出了基于LTS的仿真模型組合驗證方法，從行為方面驗證組合仿真模型的有效性。驗證過程中引入了時間因素，將組合仿真模型和請求模型的行為序列表示為LTS，通過比較二者之間的關系，驗證組合仿真模型的有效性。

雖然在建模與仿真領域，請求模型(也稱完美模型)的存在是被普遍接受的，但通過對實際系統的觀察得到請求模型的過程仍然是仿真界亟待解決的問題。此外，按任務展開次數τ值的不同對整個驗證方法的影響還需要進一步的研究，τ應該足夠大以捕捉所有偏離的行為，但是很難預先獲得最佳的τ值。

參考文獻：

[1]PETTY M D,WEISEL E W,MIELKA R R.A formal approach to composability[C]// Proceedings of the 2003 Interservice Industry Training, Simulation and Education Conference. Orlando，USA， 2003：1763-1772.

[2]WEISEL E W,PETTY M D, MIELKA R R. Validity of models and classes of models in semantic composability[C]// Proceedings of the Fall 2003 Simulation Interoperability Workshop. Orlando, USA，2003：535-541.

[3]PETTY M D,WEISEL E W. A composability lexicon[C]// Proceedings of the Spring 2003 Simulation Interoperability Workshop. Orlando,USA, 2003: 181-187.

[4]王維平,朱一凡.仿真模型有效性確認與驗證[M]. 北京：國防科技大學出版社,1998：15-18.

WANG Weiping, ZHU Yifan. Simulation model validation and verification[M]. Beijing：National University of Defense Technology Press,1998：15-18.

[5]周東祥, 仲輝, 李群,等.復雜系統仿真的可組合問題研究綜述[J]. 系統仿真學報, 2007, 19(8):1819-1823.

ZHOU Dongxiang,ZHONG Hui,Li Qun,et al. Survey of simulation composability of complex systems[J]. Journal of System Simulation,2007,19(8):1819-1823.

[6]周東祥, 李群, 王維平. 可組合仿真模型的語義形式描述及組合判定方法[J].國防科技大學學報，2008,30(1):89-92.

ZHOU Dongxiang, LI Qun, WANG Weiping. Formal representation of semantics for composable simulation models and checking rules for semantic composability[J]. Journal of National University of Defense Technology, 2008,30(1):89-92.

[7]周東祥. 多層次仿真模型組合理論與集成方法研究[D].長沙：國防科學技術大學,2007:27-43.

ZHOU Dongxiang. Multi-level simulation model portfolio theory and integration methods[D]. Changsha：National University of Defense Technology, 2007:27-43.

[8]GARAVEL H.CADP 2006: A toolbox for the construction and analysis of distributed processes[C]// Proceedings of the 19th International Conference on Computer Aided Verication.Berlin, Germany, 2007: 158-163.

[9]SZABO C,TEO Y M,SEE S.A time-based formalism for the validation of semantic composability[C]// Proc. of the Winter Simulation Conference.Austin,USA,2009:1411-1422.

[10]SZABO C, TEO Y M. On validation of semantic composability in data-driven simulation[C]//2010 IEEE Workshop on Principles of Advanced and Distributed Simulation.Atlanta, USA,2010:1-8.