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.