LTS仿真模型組合驗(yàn)證方法

馮曉寧, 王卓, 王金娜

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

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

1 模型組合驗(yàn)證方法

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

該驗(yàn)證方法主要分為4個(gè)步驟：1)行為展開(kāi)；2)行為組合；3)模型行為表示為L(zhǎng)TS；4)仿真模型的有效性驗(yàn)證，如圖1所示。前3個(gè)步驟都分別在組合仿真模型與請(qǐng)求模型上獨(dú)立執(zhí)行，第4個(gè)步驟為組合仿真模型與請(qǐng)求模型共同參與。本文將對(duì)步驟1)～3)進(jìn)行詳細(xì)說(shuō)明。

圖1 仿真模型組合的驗(yàn)證過(guò)程

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

(1)

式中：I表示輸入數(shù)據(jù)集合，Sp是當(dāng)前狀態(tài)，Δt是狀態(tài)轉(zhuǎn)換的時(shí)間間隔，狀態(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)爆炸，每個(gè)仿真模型都只考慮影響狀態(tài)轉(zhuǎn)換的通信狀態(tài)和屬性。

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

(2)

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

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

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

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

(3)

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

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

(4)

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

(5)

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

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

2 模型組合有效性驗(yàn)證

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

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

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

定義1 仿真模型強(qiáng)模擬

定義2 仿真模型強(qiáng)等價(jià)

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

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

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

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

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

(6)

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

(7)

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

(8)

(9)

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

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

(10)

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

(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]。語(yǔ)義相似度關(guān)系Vε主要考慮COSMO本體的組合狀態(tài)間關(guān)系，它以仿真模型屬性為依據(jù)。

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

(13)

3 仿真模型組合實(shí)例驗(yàn)證

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

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

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

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

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

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

3.2 坦克修理所模型展開(kāi)

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

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

則M1展開(kāi)式如下：

M2展開(kāi)式為

M3展開(kāi)式為：

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

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

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

3.3 仿真過(guò)程及有效性驗(yàn)證

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

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

(a) 組合模型LTS

(b) 請(qǐng)求模型LTS

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

4 結(jié)束語(yǔ)

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

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

參考文獻(xiàn)：

[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]王維平,朱一凡.仿真模型有效性確認(rèn)與驗(yàn)證[M]. 北京：國(guó)防科技大學(xué)出版社,1998：15-18.

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

[5]周東祥, 仲輝, 李群,等.復(fù)雜系統(tǒng)仿真的可組合問(wèn)題研究綜述[J]. 系統(tǒng)仿真學(xué)報(bào), 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]周東祥, 李群, 王維平. 可組合仿真模型的語(yǔ)義形式描述及組合判定方法[J].國(guó)防科技大學(xué)學(xué)報(bào)，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].長(zhǎng)沙：國(guó)防科學(xué)技術(shù)大學(xué),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.