馮曉寧, 王卓, 王金娜

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

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

1 模型組合驗證方法

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

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

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

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

(1)

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

驗證方法的步驟1行為展開過程基于仿真模型的執(zhí)行時間，本文將狀態(tài)機表示的概念仿真模型行為進行統(tǒng)一規(guī)范化表示為

(2)

式中：fi代表仿真模型Mi的形式化表示，表達式中t為狀態(tài)開始轉(zhuǎn)換的時刻，經(jīng)過Δt的轉(zhuǎn)換時間間隔，t+Δt為狀態(tài)轉(zhuǎn)換后的時刻。

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

驗證方法步驟2)，仿真模型行為組合主要考慮以下約束規(guī)則：任意相互組合的2個仿真模型，后者需求輸入的時間必須大于等于前者產(chǎn)生輸出的時間；“連接件的傳輸時間”必須考慮，它是一個概念上的名詞，表示相互組合的2個仿真模型數(shù)據(jù)從一方傳輸?shù)搅硪环降臅r間延遲；同一個基礎(chǔ)仿真模型，執(zhí)行第2個任務(wù)的開始時間必須大于等于前一個任務(wù)的結(jié)束時間。

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

(3)

式中：N表示節(jié)點的集合，Act表示轉(zhuǎn)換標簽的集合，→表示節(jié)點間轉(zhuǎn)換的集合。

N中的每個節(jié)點都表示一個帶有注釋的組合狀態(tài)，該組合狀態(tài)是一個三元組:

(4)

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

(5)

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

圖2 模型執(zhí)行序列和對應(yīng)的LTS

2 模型組合有效性驗證

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

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

分別為請求模型行為序列與組合仿真模型行為序列的標簽轉(zhuǎn)移系統(tǒng)。

定義1 仿真模型強模擬

定義2 仿真模型強等價

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

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

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

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

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

(6)

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

(7)

則語義相似度關(guān)系：

(8)

(9)

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

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

(10)

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

(11)

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

(12)

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

語義函數(shù)距離用于確定進入和離開LTS的函數(shù)是否相關(guān)。假設(shè)fi(p)、fjR(q)分別是標簽轉(zhuǎn)移系統(tǒng)L(M)和L(MR)中對應(yīng)的進入或離開節(jié)點p和q的函數(shù)，則語義函數(shù)距離DF(fi(p)、fjR(q))為：

(13)

3 仿真模型組合實例驗證

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

3.1 作戰(zhàn)坦克修理所

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

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

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

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

3.2 坦克修理所模型展開

根據(jù)表1中的狀態(tài)機信息，可將仿真模型M1、M2和M3的行為規(guī)范化表示為以下形式：

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

則M1展開式如下：

M2展開式為

M3展開式為：

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

得到一組滿足組合仿真模型執(zhí)行行為的時間解：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 仿真過程及有效性驗證

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

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

(a) 組合模型LTS

(b) 請求模型LTS

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

4 結(jié)束語

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

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

參考文獻：

[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]周東祥, 仲輝, 李群,等.復雜系統(tǒng)仿真的可組合問題研究綜述[J]. 系統(tǒng)仿真學報, 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].長沙：國防科學技術(shù)大學,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.