实时分布仿真的性能评估基于概率模型检测技术

理论计算机科学电子笔记128（2005）3-24www.elsevier.com/locate/entcs基于概率模型检测Jeremie BonteDTIM，ONUCENATIONALD'E'tude set摘要本文的目标是展示如何使用概率模型检测技术，以实现定量的实时分布式仿真的性能评估。基于高层体系结构（HLA）的仿真建模为一个随机过程，连续时间马尔可夫链（CTMC），使用随机代数PEPA。接下来的属性表示的性能约束进行评估，应用连续随机逻辑CSL公式的CTMC模型，使用概率模型检查PRISM。最后，对模型进行了初步实验，并与实际案例进行了比较。关键词：实时分布仿真，概率模型检测，性能评估，PEPA，PRISM。1介绍实时模拟在很大的时间限制下。实时仿真的特殊性在于仿真的逻辑时间必须与真实时间一致。为了保持真实时间和逻辑时间相等，仿真的计算为了获得足够的计算能力，一个模拟通常被分成几个较小的模拟，分布在不同的机器上。不幸 的 是 ， 较 小 的 模 拟 失 去 了 系 统 的 全 局 高 层 体 系 结 构 （ High LevelArchitecture，HLA）是一个致力于实现这些功能的1电子邮件：nil. cert.fr1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.0104N. Geisweiller，J.Bonte/Electronic Notes in Theoretical Computer Science 128（2005）3由网络承载的数据交换。这里的问题是网络和中间件在它们的通信中引起了一些延迟，这可能会妨碍仿真的真实性。为了知道分布式仿真是否正确运行，需要检查某些时间约束本文的目的是展示如何将分布式仿真建模为概率过程，以便使用概率模型检查技术来验证系统是否满足某些所需的约束由于系统的内在性质，这些约束不能总是成立，但可以预期在大多数情况下，这些约束都是合理的。概率模型允许量化这种信心，并允许以更简单的方式表示复杂的行为。例如，在网络建模中，不需要对消息如何丢失进行建模，而只需对消息丢失的概率进行建模。为了实现这一目的，HLA分布式仿真建模的随机过程，连续时间马尔可夫链（CTMC）。然后，连续随机逻辑（CSL）是用来正式的性能约束所需的模拟行为正确。概率模型检查器PRISM允许CTMC模型的构建和CSL公式是否满足CTMC模型的验证。本文其余部分的组织如下。第二部分回顾了本文所需的基本概念：高层体系 结 构 （ HLA ） 、 连 续 时 间 马 尔 可 夫 链 （ CTMC ） 和 随 机 算 法 PEPA（Performance Evaluation Process Algebra）、连续随机逻辑（CSL）和软件PRISM。第三部分描述了一个基于HLA的实时分布仿真实例，详细说明了用PEPA对CTMC进行建模的方法。第4节包含CSL形式化的时间约束，需要通过模型进行验证，第5节使用模型检查器PRISM获得结果。 第六节是与模型和实际仿真案例的比较。最后，第7节给出了一些结论和未来的工作方向。2基本概念2.1HLA体系结构高层体系结构（HLA）提供了一个通用技术体系结构的规范，将多个仿真组合成一个更大的仿真。N. Geisweiller，J.Bonte/Electronic Notes in Theoretical Computer Science 128（2005）35它为仿真互操作提供了结构基础。创建的组合仿真称为联邦，组合形成联邦的每个仿真称为联邦成员。所有联邦成员都通过一个名为RTI的软件互连。RTI负 责通 过 网络 进 行的 所 有通 信 ，网 络可 以 是局 域 网（ LAN ） 或广 域 网（WAN），如Internet。RTI必须保持仿真的一致性。它有两个主要功能，对象管理和时间管理，但在实时仿真的情况下，时间管理是不使用的。对象管理器的快速描述可以在下面找到成员可以发布或订阅对象类。对象类的发布者可以注册该类的对象实例，然后联邦成员被称为注册对象的所有者。每个对象都有一组属性，当模拟运行时，所有者可以更新对象的属性值（UAV）。最后，RTI将新属性2.2有限连续时间马尔可夫模型分布式仿真已建模在连续时间马尔可夫链（CTMC）。在本节中，将介绍CTMC的定义，解释如何使用CTMC获得非指数分布以及为什么选择此类模型来描述实时分布式仿真。马尔可夫过程是一个没有记忆的随机过程。这意味着进行转换的概率仅取决于当前状态，而不取决于过程的过去。 注意，任何过程都可以表示为马尔可夫过程，包括过程在每个当前状态下的历史。然而，这可能意味着状态的数量可能是无限的（可能是不可数的），这可能很难验证。有限连续时间马尔可夫链（CTMC）是定义连续时间域中的马尔可夫过程的有限图下面是有限连续时间马尔可夫过程的定义。更多的细节可以在[10]中找到。定义2.1LetSbeaftatetftee ra t或matrix，v ec t或E：S<$→R+，E（s）=sJ∈SQ（s，SJ）.Leti：S<$→[0，1]be一个概率分布叫做初始分布。连续时间马尔可夫过程是一个随机过程X=（Xt）t∈R+，定义如下：6N. Geisweiller，J.Bonte/Electronic Notes in Theoretical Computer Science 128（2005）3ΔtE（ s）E（ s）S212 5S14S3Fig. 1. 连续时间马尔可夫链概率定律：• s∈S，P{X0=s}=i（s）• s，sJ∈S<$t，<$t∈R+，P{Xt+ Xt= sJ|Xt= s}=其中lim_t→0o（lim_t）= 0⎧如果s/=sJ，则为<$Q（s，sJ）×<$t+o（<$t）<$1−（E（s）+Q（s，sJ））×<$t+o（<$t）ifs=sJ上述定义通过相对于时间的概率无穷小变化来描述系统的行为。该过程的全局行为是通过求解微分方程组得到的因此，停留在状态S1根据相对于时间的指数递减函数而减小从微观的观点来看，Q（s，SJ）表示假设系统处于状态s时，向状态SJ跃迁的增长系数。它也对应于全局的平均频率采取过渡（s，sJ）。因此，在进行转换之前花费的平均时间（以s为单位）为1。 从状态s移动到s'的概率一个跃迁，记为P（s，SJ），如果E（s）= 0，P（s，sj）=0，则P（s，sj）=Q（S，SJ如果E（s）= 0。例如，定义为S={s1，s2，s3}的马尔可夫过程，I（s1）= 1，I（s2）=I（s3）= 0，Q（s1，s2）= 2，Q（s1，s2）= 4，Q（s2，s3）=5Q（s3，s3）= 1，Q（s1，s1）=Q（s2，s1）=Q（s2，s2）= 0 =Q（s3，s1）=Q（s3，s2）=0（参见图1为相应的图表），遵循概率分布P{Xt= s1}= e−6t，P {Xt= s3}= 1+ e−6t−2e−5t，P {Xt+tJ = s3|Xt= s3}= 1，P{Xt+tJ= s1|Xt= s3}= P {Xt+tJ = s1|Xt= s2}= 0。然后考虑具有初始状态si的CTMC，这意味着初始分布i使得对于所有si=si，i（si）= 1且i（s）= 0。通常，CTMC的状态由有限的有界变量集描述，例如布尔、有界整数或枚举。因此，状态空间由每个变量域的笛卡尔积定义。这些变量称为状态变量。N. Geisweiller，J.Bonte/Electronic Notes in Theoretical Computer Science 128（2005）37具有无记忆属性的描述的结果是，从当前状态进行转换的唯一类型的分布是指数分布。然而，通过并行或串联组成有限数量的状态，可以近似任何分布（更多细节见[9]这是在第3.3节中为网络建模而做的。因此，尽管马尔可夫过程具有无记忆性，但仍然可以表示（或近似）一般分布，而无需生成无限数量的状态。这个重要的事实允许模拟复杂的随机过程与现实的分布，然后在模型上应用概率模型检查技术。2.3绩效评估流程代数PEPAPEPA作为性能评估过程代数是由Hillston [6]定义的随机过程代数，其允许描述任何有限CTMC。PEPA可以被看作是通信系统计算（CCS）[8]或通信顺序过程（CSP）[7]的连续时间概率扩展。定义2.2设A是一组动作名称。τ设计未知动作，T设计未知速率。PEPA中术语的语法定义如下：P=（α，r）.P |P da Q|P + Q|P/L|P [l]|一L（α，r）.P是Prefix运算符，表示相关CTMC的基本转换，α是动作名称，r是进行转换的速率tion和P是进行转换后的过程的描述。 P da Q，L协作算子，是两个过程P和Q在协作动作集L∈ A\{τ}上的同步积。P + Q是最佳的运算器。P/L是一个隐藏算子，它保持了进程与其他进程之间属于L的交互。 P[l]是操作重命名操作符，ldefB是一个映射A→。AA是由A=P定义的任何常数。给定的PEPA项设计了某个CTMC，相关的CTMC通过两个步骤得到：(i) 得到了由一组Plotkin风格的语义规则（称为PEPA的操作语义[6]）诱导的派生图。基本上，派生图是在转换上添加了动作名称的CTMC(ii) 通过消除动作，从导出图中获得CTMC8N. Geisweiller，J.Bonte/Electronic Notes in Theoretical Computer Science 128（2005）3（τ，5）.Final da Loop（τ，2）{α}（α，5）（α，1）首字母da Loop关于我们（α，4）最终da Loop关于我们图二. PEPA项模型转换的名称和集中等效转换。操作语义是相当标准的，在这里不回顾（参见[6]以获得进一步的解释）。 在论文的案例研究中，只有主动（已知速率）与被动（未知速率，记为T）转换的同步，用了这种同步的语义非常简单，因为结果转换速率仅由主动转换速率定义例2.3使用PEPA形式定义图中的CTMC1如下所示：def• 模型=初始da循环关于我们• 初始def=（τ，2）。（τ，5）. Final+（α，4）. Final• 菲纳尔def=（α，1）.def• Loop=（α，T）.Loop状态空间由操作语义学引入的项构成P E P A 从长期模型。相应的推导图见图2，相应的CTMC见图1。2.4连续随机逻辑CSL连续随机逻辑（CSL）在文献[1]中被引入，将CTMC上的一类属性形式化。CSL是PCTL（ProbabilityComputationTree Logic） [5]的连续时间扩展，PCTL是CTL（ComputationTree Logic） [2]的概率扩展。它的性质允许表达具有某种行为的概率满足区间[0，1]中的某个界限。CSL的简短定义如下。定义2.4CSL公式具有以下语法Φ：：=true aΦΦ <$Pdap[]Sdap[Φ]：：=X ΦXI Φ ΦU ΦUI ΦN. Geisweiller，J.Bonte/Electronic Notes in Theoretical Computer Science 128（2005）39其中da∈ {<，≤，>，≥}，p∈ [0，1]，I是R的一个区间. Φ表示a表示状态公式，并且k表示路径公式。语义如下。• 状态公式在具有初始状态（也称为当前状态）的CTMC上进行解释· 真实总是令人满意的。· a是一个原子公式，通常是一个简单的命题变量。当原子公式在当前状态下的解释为真时，它就被满足了· 布尔运算符（resp. ）对应于逻辑和（resp. 不）。· 当从当前状态开始的路径集合的概率测度满足路径，满足概率公式Pdap[k]。式III满足结合DA P。· 稳态公式Sdap [Φ]在时间趋于无穷大时处于满足Φ的状态的概率满足界限da时满足。 这个界限总是有定义的，见[10]。• 给出了CTMC上的一个路径公式和一条路径σ.· 当σ的第二态满足Φ时，下一个公式X Φ满足。· 当σ的第二个状态满足Φ，并且到达这个状态的时间在区间I内时，下一个有界公式XI Φ就满足了。· 如果在路径σ的长距离上，直到满足Φ 1，直到满足Φ 2，则直到满足公式Φ 1U Φ 2。· 有界直到公式Φ1UI Φ2具有与直到公式相同的语义。公式，但从开始到达Φ2I.例如，系统在100s之前丢失消息的概率低于0.01的属性可以简单地形式化为：均0. 9 [真U <0. 001F edCgota↑]5PRISM结果这个模型的描述已经写在概率模型检查器PRISM中。系统的特性可以通过一些参数来调整，如UAV消息的长度、容纳RTIG的机器的速度和网络的吞吐量。然后可以检查是否根据所选参数验证了时间约束。重要的是要认识到，模型的参数和现实的参数之间的关系并不十分直接，实际上模型是对现实的抽象20N. Geisweiller，J.Bonte/Electronic Notes in Theoretical Computer Science 128（2005）3最后期限遵守的概率取决于吞吐量10.90.80.70.60.50.40.30.20.1002e+074e+076e+078e+071e+08 1.2e+08以位/秒为单位见图6。 与吞吐量现实和许多细节没有被明确地描述，例如通信协议的不同级别。因此，有必要校准模型的所有速率，如果模型的参数值和现实的参数值相同，则它们都给出相同的结果。通过以模型的速率添加系数并改变它们，直到模型与现实对于给定的一组参数值一致，简单地完成校准。在本案例研究中，仅考虑了长度的尺寸，以根据实际情况校准模型。然而，在这个维度上，模型给出了良好的预测结果（见第6节）。因此，由模型给出的关于RTIG的速度和网络的吞吐量的结果仅仅是理论上的，并且可能没有给出预期的现实结果。本节的图表显示了在消息行程的持续时间内遵守截止日期的概率，该概率与RTIG的速度、网络的吞吐量和UAV的长度等不同这些结果已经计算使用一个额外的CSL运营商提供的PRISM允许计算的概率测量的一组执行验证某个属性。这些性能评估的结果如上图所示图6和图7示出了根据网络的吞吐量和RTIG的速度的最后期限遵守的概率图8显示了验证遵守最后期限的概率，根据最后期限的时间从0 ms到1 ms变化，以及UAV的三种不同长度，64，256和512个八位字节。概率N. Geisweiller，J.Bonte/Electronic Notes in Theoretical Computer Science 128（2005）321遵守最后期限的概率取决于RTIG的速度10.950.90.850.80.750.70.650.62000400060008000 100001200014000 16000任意单位见图7。 PRISM结果与RTIG不同无人机长度10.90.80.70.60.50.40.30.20.100 0.2 0.4 0.6 0.8 1截止期限时间x 10−3见图8。关于潜水员长度6第一次与真实案例本节包含模型与真实系统的第一次比较。在两台由100 Mbits/s全双工电缆连接的机器上进行了实时仿真。 在模型中，系统由三个联邦成员和RTIG组成。为了测量在相同的时钟下将无人机从一个联邦成员发送到另一个联邦成员的持续时间，三个联邦成员被安置在同一台机器上。RTIG一直由英特尔奔腾41500 MHz的住房和联邦一直由四处理器英特尔800 MHz的住房。这第一个实验提供了有用的信息来校准模型的转换速率。图9、图10和图11显示了在不同长度的无人机上模型与实际情况的比较。看来这个模型很好地近似了现实概率长度=64octs长度=256octs长度=512octs遵守期限的概率22N. Geisweiller，J.Bonte/Electronic Notes in Theoretical Computer Science 128（2005）3模型与现实，长度=64octs10.90.80.70.60.50.40.30.20.100 0.2 0.4 0.6 0.8 1截止期限时间x 10−3见图9。 模型与现实，长度=64octs模型与现实，长度=256octs10.80.60.40.200 0.2 0.4 0.6 0.8 1截止期限时间x 10−3见图10。 模型与现实，长度=256octs在不同的长度上。已经观察到，选择Erlang-k分布来模拟网络，而不是基本的指数分布，极大地促进了模型的真实性7结论和今后的工作采用过程算法PEPA，将基于高层体系结构HLA的实时分布仿真建模为连续时间马尔可夫链。在CSL中对从一个联邦成员向另一个联邦成员传输消息的持续时间的时间约束进行了形式化，并在不同的参数值上使用模型检查器PRISM进行了验证。对联邦成员交换的不同长度的消息进行了第一次实验，并在这些值上给出了良好的结果现实模型现实模型概率截止期概率截止期