多形式建模：有效解决复杂系统中的问题和性能评估

可在www.sciencedirect.com在线获取理论计算机科学电子笔记296（2013）61-77www.elsevier.com/locate/entcs多形式建模Enrico Barbierato1DI，Universit`adegliStudidiTorinocorsoSvizzera，185，10129 Torino（Italy）Gian-Luca DeiRossiDAIS，Universit`aCaVia Torino，155，30172 Mestre Venezia（Italy）Marco Gribaudo3DEI，Politecnico di Milanovia Ponzio 34/5，20133 Milano（Italy）Mauro Iacono4DSP，SecondaUniversit'adegliStudidiNapoliviale Ellittico，81100 Caserta（Italy）安德烈·马林5DAIS，Universit`aCaVia Torino，155，30172 Mestre Venezia（Italy）摘要多形式主义建模已被证明是一种有价值的技术，以应付复杂的约束，适用于规范的基于计算机的系统的最先进的状态。多形式主义技术帮助建模人员和设计人员提供一个更（自然和）方便的方法，在规范的过程中，并在性能分析。虽然它们的应用并不一定在模型的解决方案中提供优势，但本文展示了组合多形式主义建模方法如何利用乘积形式解决方案的力量，为复杂系统提供有效的解决方案和具体的模型关键词：多形式建模，产品形式解决方案，组合性，性能评估1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.07.00562E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）611引言基于计算机的系统每天为大多数人类活动提供服务，其特征是复杂性水平不断提高，这一术语可以以不同的方式解释。复杂性可以在这些系统在运行时必须满足的并发要求中找到（例如，对于具有时间，安全性，可靠性和性能约束的关键系统），从它们的不同关节的数量，或从它们的扩展。此外，复杂性可能是由现有子系统组成的实体设计逻辑的结果。在所有这些情况下，设计师面临的挑战是利用模型来定义或理解系统多形式主义建模技术允许建模者选择最合适的建模形式主义来主导整个系统模型的不同方面或部分，从而提供更易于管理和理解的支持。这种自然的模块化支持基于组件的divide-et- impera方法，但并不意味着更有效的模型解决方案。基于状态空间的模型分析技术源于所谓的状态空间爆炸问题。模块化已经在文学中被不同地利用来面对这个问题，这表明适当的子模型组合管理可以有效地产生解决方案。模拟可以扮演银弹的角色，但代价是可能需要更长的计算时间。 在许多情况下，可以通过依赖组合物结构的特定特征或引入适当的人工方法来生成有效的分析解。这是乘积形式求解技术的情况，这超过了许多已知的情况，在这些情况下，复杂模型的分析可以通过分析其组件来获得在本文中，我们展示了如何产品形式的解决方案理论很容易耦合与多形式主义的组合建模技术，以获得一个建模和分析框架，oamerers建模的灵活性和有效的解决方案。本文的贡献是建立在一个可扩展的建模和解决方案框架的设计和实施，支持的工具解决多形式马尔可夫模型的三重解决方案机制。该工具自动验证并执行产品形式的解决方案。如果这不可用，则提供基于状态空间的分析解决方案或仿真作为最终的备份工具。该研究扩展了SIMTHESys的框架，1enrico. mfn.unipmn.it2deirossi@dais.unive.it3gribaudo@elet.polimi.it4mauro. unina2.it5marin@dais.unive.itE. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）6163[1]中提出的产品形式解决方案工具，以涵盖ERCAT/MARCAT产品形式模型。到目前为止，似乎没有其他类似的，工具支持的方法在当前的文献。在论文的其余部分，第2节介绍了在这项工作中介绍的方法，第3节展示了一个案例研究，第4节介绍了一些相关的工作，多形式主义建模和产品形式的解决方案。结论见第5节。第2章从多形式主义模型到乘积形式解本文提出的方法利用现有的模块化的多形式主义模型和SIMTHESys框架的可能性，利用马尔可夫链产品形式的解决方案检测在一个多形式主义的解决方案的过程。SIMTHESys框架支持设计和开发用户定义的形式主义，并自动生成适当的（多）形式主义该框架定义了一种形式主义设计技术，基于元建模和一种指定形式主义每个元素的结构和动态特征的机制[4，6，5]。求解器生成基于对形式主义描述的分析和一组基本求解引擎，其中基本应该旨在能够实现基本的求解技术。在本文中，马尔可夫链求解引擎（分析和模拟），连同一个新的求解引擎，受益于INAP算法和MARCAT定理。一组规格，（多）形式主义应满足MARCAT模型将通过开发一个适当的例子高级形式主义。我们引入了一个新的形式主义家庭，这是一组新 这一系列形式主义的特征 受到具有主/从同步的连续时间随机自动机网络中可用功能的启发[10]。 这个新的形式主义家族将被称为标记指数事件形式主义。属于这个家族的形式可以方便地认为是标记指数自动机。该方法是通过使用SIMTHESysER，SIMTHESys框架求解器生成工具，和INAP，一个工具，自动检测的许多产品形式的解决方案的基础上MARCAT算法。在这种方法中，所提出的形式主义家族允许i）SIMTHESys框架生成基于产品形式解决方案的优化求解器，ii）INAP支持高级形式主义，将其应用领域扩展到更复杂的模型。此外，这两个工具整合的另一个结果是，通过自动验证以下信息，丰富了MARCAT的好处：64E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）61它的假设，使用SIMTHESysER状态空间生成逻辑。这提供了一种工具，允许识别更多已知的产品形式，而不需要逐个检查它们该方法的主要限制是它只适用于模型两两合作因此，不考虑更复杂的产品形式，例如基于瞬时信号传播的产品形式[16]。当产品形式不适用时，模型由生成的求解器使用一般分析方法求解，或通过模拟求解。2.1产品形式解的确定与计算在本节中，我们概述了决定模型是否接受基于MARCAT的乘积形式解决方案的主要步骤，以及在肯定答案的情况下计算它。属于本工作中考虑的标记指数事件形式主义的模型可以被认为是元组（C，L），其中C ={c1.. cN}是子模型组件的集合，并且L ={11. lK}是一组标签。子模型可以用属于所考虑的家族的任何形式主义来定义具体地，每个子模型分量ci由变量Vi={vi，1. iEi={ei，1. ei，mi}，其支配从一个状态到另一个状态的转变。每个状态Si由其变量的值唯一标识：如果两个状态对于模型的所有变量都有相同的值，它们是相同的状态。状态Si中包含的信息能够完全定义可能导致状态变化的事件ei∈Ei触发状态改变的事件可以在本地发生，称为指数分布时间，或者由于同步而称为全局时间。指数级事件ei以速率λ（ei，Si）→R+表征：当系统进入状态Si时，事件ei将在一个指数分布的随机时间量之后发生，速率为λ（ei，Si）.如果在相同的状态Si中可以发生多于一个事件，则使用竞争策略在标签上遵循主/从范例执行同步。活动事件有一个指数时间和一个标号：μ（ei，Si）→R+×L。被动事件只有一个与之相关的标签：γ（ei，Si）→L。当活动事件在某个状态下可用时，它会在相应的指数分布随机时间量之后触发。在活动事件的执行期间，生成相关联的标签lj。相反，一旦由另一子模型中的主动事件生成对应的标签l，j，所有的事件都将系统移动到另一个状态，通过适当地改变定义事件所涉及的各个子模型状态的变量的值（即，控制器的状态E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）6165我对于局部事件，或者对于其中活动和事件是长的子模型，有边的子模型，即SJ=f（ei，Si）<$si∈S。为了保持本文的独立性，我们简要地介绍了MARCAT的情况下，一对合作的模型Pc1和Qc2（在这种情况下，该定理通常被称为ERCAT）。我们用PQ表示联合模型。假设对于每个标号a，我们知道一个正实值xa，设PJ（QJ）是过程P（Q），其中所有标号为a∈ PP（a∈ PQ）的被动转移都以xa为速率。显然，PJ和QJ现在是独立的，如果基本的CTMC是遍历的（或有一个遍历的状态子集），我们可以计算它们的稳态分布πP′和πQ′。根据MARCAT，存在乘积形式解，如果对于P<$Q的（p，q）的每个遍历状态，我们有其稳态概率π（p，q）为：π（p，q）<$πP′（p）πQ′（q），其中如果P<$Q的遍历状态是PJ和Qj的遍历状态的笛卡尔积，则正比例符号是等式。下面的集合在MARCAT的应用中起着关键作用，我们记得（p，q）是PQ的遍历状态：(i) P（p，q）→是从（p，q）输出的被动标签的集合(ii) A（p，q）→是从（p，q）传出的活动标签的集合(iii) P（p，q）←是进入（p，q）的被动标签的集合(iv) A（p，q）←是进入（p，q）的活动标签的集合MARCAT给出了一种纯算法的方法来判定两个过程合作的乘积形式解的存在性，并在存在的情况下给出了其表达式。定理2.1（MARCAT[18]）设P和Q是标签集L上的两个合作过程，并假设满足以下条件• 对于每个标号a∈AP（a∈AQ），xa是PJ（QJ）中所有标号为a的跃迁的反转率• 对于每个关节状态（p，q），以下速率方程成立：Σa∈P（p，q）→xa−ΣXaa∈A（p，q）←Σ=βa（p，q）−Σαa（p，q）（1）a∈（P（p，q）<$zA（p，q）<$）a∈（A（p，q）→zP（p，q）→）其中αa（p，q）是从状态（p，q）出发的跃迁速率，（p，q）而βa是跃迁进入（p，q）的反转速率标记为a;则对于联合过程的每个遍历状态（p，q）66E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）61保持：π（p，q）<$πP′（p）πQ′（q）在实践中，MARCAT的适用需要解决以下问题：• 确定每个同步标签的值xa• 针对联合模型的每个遍历状态检查等式（1）。特别地，β a值的计算需要知道a为无源的部件的稳态分布;在这里，第一个问题通过应用INAP [21]解决，假设乘积形式存在，我们检查方程（1）的后验。INAP输出包含反向速率的值和孤立的每个组分的稳态分布。因此，该信息用于在给定的数值精度内验证MARCAT速率条件（1）2.2形式主义SIMTHESys是一个灵活的工具，允许根据用户的需求和专业知识定义各种在这里，我们只介绍在第3节的案例研究中使用的两种形式。第一个是开放的、有限容量的、阻塞的、重复服务排队网络的变体，正如我们已经看到的;第二个是随机Petri网的变体：这两种形式主义都通过包含实现给定规范的元素而得到丰富。这两种形式主义的元素都在图。1.一、对于排队网络，除了以其容量、长度和服务速率为特征的队列元件之外，排队网络形式体系还具有六个其他节点元件：源元件生成请求并以其速率为特征;主动源元件以其速率生成请求并输出标签;被动源元件以取决于绑定标签的速率生成请求;宿元件消耗请求;主动宿元件消耗请求并输出标签;被动宿元件消耗取决于绑定标签的请求。形式主义也有arc元素（在源、队列和sink之间路由请求）、test arc元素（检查节点元素上的条件以启用另一个节点元素）和inhibitor arc元素（根据另一个节点元素的状态禁止节点元素子模型的状态简单地由队列的占用率定义。本地事件用于说明队列中服务的结束以及到达系统的活动事件用于考虑从具有关联标签的汇（活动汇）离开系统，以及从活动源到达系统被动事件被用来模拟被动到达和被动离开：前者对应于系统中的到达，该到达是由属于E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）6167队列S源S水槽P被动源P被动离开一活动源一主动离港电弧测试电弧抑制器电弧地方过渡被动过渡活性过渡电弧测试电弧抑制器电弧to a different不同sub-子model模型.后者指由于来自不同中断源的中断，客户立即离开系统此外，由于测试弧和抑制弧，当相邻站的总队列长度（但总是在相同的子模式中）变得大于或小于给定的阈值时，队列、源和宿可以被阻塞。QN原语SPN原语Fig. 1. 形式主义要素网络的语义就是这样实现的。首先，通过查看各个站的队列大小来确定启用事件。所有Source和Active Source原语始终生成一个事件（前者是本地事件，后者是活动事件 被动源生成被动事件。如果相应的队列至少有一个客户，则队列原语生成事件。如果队列的目的地是另一个队列或接收器，则事件是本地的;如果目的地是主动离开，则事件是主动的;如果目的地是被动离开，则事件是被动的。随机Petri网形式主义有四个节点元素：位置元素，以其标记为特征;过渡元素，以其速率为特征;主动过渡元素，以其速率和其导出的标签为特征;被动过渡元素，其速率取决于绑定标签。该形式主义具有类似于排队网络形式主义的弧元素。Active Transitions的行为完全符合标准SPN定时转换，但它们在触发时也会暴露标签。相反，被动转换完全由其他子模型中发生的主动事件控制Petri网通过为每个启用的转换生成事件来实现。特别地，所生成的事件的类型对应于转换的类型：用于标准转换的本地事件、用于主动转换的主动事件以及用于被动转换的被动事件。请注意，在我们的方法标签中，主动和被动事件用于68E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）61提供一个形式独立的合作方案，允许子模型之间的同步，使用不同的建模语言指定在封闭的主模型中使用合作弧连接子模型每个协作弧都关联了一组标签，并且它从源子模型指向目的地子模型：每当具有对应标签的主动事件在源子模型中发生时，它就会触发目的地子模型中与相同标签相关联的启用的被动事件。3为例在本节中，我们将介绍一个使用所提出的工具进行分析的示例。请注意，该系统已被选定为发现本文所述技术一个用于地震现象检测和监测的数据流处理系统由两个主要子系统构成：预处理子系统和临界检测子系统。第一个由两个阶段组成，每个阶段用一个时间变量计算来处理批次，其持续时间是指数分布的。这两个阶段接收不同的工作要处理，具有指数分布的速率。此外，第二个接收第一个输出批次的一部分，第二个处理的一些作业被送回第一个处理，而其他作业则构成子系统的输出。每个阶段都可以创建多个带时间戳的作业。不允许将作业分发到下一个阶段的阶段必须重新处理数据，以考虑所花费的时间。第二个子系统处理第一个子系统的输出作业，以及发送给它的其他作业。为了保护这个关键的子系统，当作业的数量大于固定阈值并且检测到过载情况时，保护机制可以临时关闭它。在这种情况下，新的就业机会受阻，出现损失。保护机制由适当的子系统提供3.1总体模型描述图2给出了系统的高级概念模型。第一个子系统可以用一个两节点的具有有限容量和重复服务阻塞的网络来描述，这种类型的网络在[2]中已经研究过。第二个子系统可以用一个由ON/OFF开关元件控制的有限容量队列来描述，当队列中的作业数不小于阈值m时。图中，λ1、λ2和λ3表示工件到达率;B1、B2和B3是队列的容量μ1、μ2和μ3是作业服务。p是将已处理的作业从第一个转发到第二个的概率。E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）6169第二个队列;q是从第二个队列向第一个队列转发已处理批次的概率;n是第三个队列中的作业数;γ表示ON/OFF阻止从第一个子系统向第二个子系统转发的触发器，假定n≥m。3nB3块开/关图二. 总体模型描述3.2型号规格第一个子系统由具有有限容量和重复服务阻塞的网络建模。参考图2，第一阶段由图3中的子模型QN1描述。速率为λ 1的源表示外部到达，速率为qμ2且输出标签为a的活动源表示从第二阶段到达的作业（μ2是第二阶段的服务速率，q是作业在第二阶段得到服务后进入第一阶段的概率）。 sink表示离开系统的作业，被动离开导入标签b表示可进入第二阶段的作业，容量为B1且速率为（1-p）μ1的队列表示处理单元。队列速率表达式的结果是，这里唯一可以定义的速率是sink的离开速率，因为第二阶段的离开速率取决于第二阶段的行为（参见[2]）。第二阶段由图3中的子模型QN2描述。与第一阶段类似，速率为λ2的源代表外部到达，速率为pμ1且输出标签为b的主动源代表来自第一阶段的作业，汇代表离开系统的作业，被动离开输入标签为a的队列代表第一阶段可用的作业，容量为B2且速率为（1−q）μ2的队列代表处理单元。此外，第二阶段还具有速率为γ的源，由队列通过检查其是否包含小于m的测试弧启用未决请求和导入标签C的被动离开。第二个子系统由两个随机Petri网子模型建模。图2中的第三队列由图4中的子模型SP1描述。具有速率λ3和导出标签d0的活动转换表示外部到达，并且如果左侧位置（最初标记有B3令牌以表示12312p1-qn mB1-pQ1B270E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）613321BaB(a) QN1C(b) QN2图三. QN子模型d0第一季第一集(a) SPN 1（b）SPN 2见图4。 SPN子模型有限容量）被标记，并且正确的位置（由相同的活动转换标记并且表示正在处理的请求）没有被标记。的速率为λJ导出标签d1表示外部当队列的长度至少为m时到达，标记正确的位置，并且如果左侧位置被标记并且如果右侧位置具有至少m个令牌（因此队列长度至少为m）则被启用;被动转换导入标签c表示来自第一子系统的到达，并且当左侧位置被启用并且右侧位置被标记有小于m个令牌（因此队列长度小于m）时被启用;具有速率μ3的主动转换，并且导出标签e0表示当队列小于m+1。速率为μJ的主动跃迁和出口标签e1表示当队列长度为至少m+ 1。当队列长度至少为m时，被动转换导入标签c、g和h授权来自第一子系统和ON/OFF机制的传入请求。ON/OFF子模型由两个位置描述，表示ON（左）和OFF（右）条件。具有速率δ和输出标签h以及具有速率δ和输出标签g的活动转换分别表示S（1-p）B1PS（1-q）B2MP一S PSq2一S第1页一3d03e0B3MM+1MCCGHMMM+1M+1D1e1HGE. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）6171开关0 - 1和开关ON;当左边的位置被标记时，被动转换导入标签D0、D1、E0和E1图5显示子模型如何通过桥模型连接。特别地，每个子模型被绘制为矩形，并且模型之间的协作由弧表示。箭头从执行主动转换的子模型指向受被动事件影响的子模型。主动事件标签在OUT关键字附近以黑体书写，而被动事件标签在IN关键字附近以斜体书写。输入输出输入d0，d1，e0，e1SPN1c g，hC一QN2B一QN1Bd0，d1，e0，e1SPN2h、g出来在外层在IN出来图五. 子模型组成3.3模型分析和结果SIMTHESysER为本例中考虑的模型产生的输出如图所示6，并表示在标记指数自动机，其中符号T表示被动转换。注意，依赖于全局平衡方程组的解的蛮力分析可能是不可行的。实际上，虽然有限，状态空间的基数增长为O（B1B2B3），其中Bi是第i个队列的容量为简单起见，假设Bi= B，用高斯消去等效方法得到的全局平衡方程组的标准解具有O（B9）的时间复杂度，这对于所涉及算法的数值稳定性也可能很快成为惩罚性的。 模拟可能是估计模型性能指标的另一种方法。然而，我们应该注意到，模拟估计的精度强烈依赖于模型的参数。事实上，有些事件可能很少发生，例如队列饱和或为系统保护而实施的阻塞机制 因此，可能需要时间昂贵的模拟，并且估计值的验证起着重要作用。将产品形式分析应用于该模型并非易事。事实上，参与合作的子模型都不是准可逆的，因此避免了稳态分布推导的繁琐。由模型QN1和QN2组成的带反馈的递归网络不允许Jackson乘积形式，因为站具有有限容量。尽管如此，它们的速率依赖性乘积形式依赖于[2]中进行的分析QN2的输出过程馈入SPN1;这个过程与到达SPN1的外部信号相结合满足RCAT条件。最后，亲-72E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）61λ2λ21B2c，μ2（1−q）c，μ2（1−q）a，μ2 qa，μ2qQN1b、Tb，μ1 pb、Tb，μ1 pc，γQN2a、Td，λ3d，λ3a、Td，λ3d，λ3SPN 1g，c，g，h，Tc，g，h，Tc，g，h，TSPN2d，d1，e，e1，Th，δ图第六章SIMTHESysER生产的标记指数自动机调节阻塞保护机制（SPN2）和SPN1之间交互的cess这些类型的乘积形式的组合具有由以下命题给出的非平凡解。命题3.1如果满足以下速率条件，则案例研究模型具有乘积形式解：（1−p）qλ2=（1−q）pλ1（2）γ=λ1（1−q）（λ2+pμ1）λ1（1−q）+（1−λ1λ11B1μ1（1−p）μ1（1−p）c、Tc、Tc、Tc、T1mm1B3e，μ3e，μ3e，μ3e，μ3NE. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）6173p）qμ1（三）证据可以用代数方法证明，当且仅当条件（2）和（3）满足时，方程组（1）才满足Q74E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）61如命题3.1所示，案例研究模型的乘积形式解析解取决于某些利率的选择。虽然从建模的角度来看，这有点令人失望，但其重要性不仅仅是理论上的。例如，可以应用模型的乘积形式参数化来验证模拟结果，或者在速率条件不满足的情况下，可以进行近似分析INAP单独数值求解模型，然后检查SIMTHESys计算的每个遍历联合状态的条件1）。孤立的模型解的时间复杂度与每个解的立方成正比。队列容量，因此如果B1=B2=B3=B，我们有O（kB3），其中k是在一定精度内收敛所需的迭代次数。在我们的实验中，我们观察到k≤9的所有参数化，我们尝试。由于关节状态中的转变的稀疏性，条件1可以是在常数时间检查每个联合状态，因此导致总的时间复杂度为O（B3）。我们可以得出结论，在这种情况下，乘积形式分析将解决方案的时间复杂度从O（B9）降低到O（B3）。4相关作品4.1多形式主义建模在文献中可以找到多种形式主义建模的不同方法：首先，松散的分类建议可扩展或不可扩展的框架。在第一类中，SHARPE [24]，SMART [9]和DEDS [7]是关键参考，而AToM3[11]，Müobius[23]，OsMoSys[25，13]和SIMTHESys[20，19]属于第二类。SHARPE是一个建模框架，能够研究马尔可夫模型，以产品形式表示的嵌入式网络和广义随机Petri网。SMART是一个用于设计复杂离散状态系统的软件包;它提供了数值求解算法和离散事件仿真技术。DEDS能够通过创建到通用抽象符号的转换来集成根据不同形式主义定义的模型，而AToM3则利用元建模来实现模型转换。解算器用于解算模型。莫比乌斯公司成立于1999年，是一家专业从事汽车零部件研发、生产和销售的公司。城市网络（SAN），Petri网，马尔可夫链和性能评估过程代数（PEPA），并提供了一个非常清晰的复杂模型组合技术，允许生成优化的解决方案。OsMoSys可以创建多形式化模型，并使用工作流管理来实现多解决方案，依赖于模型和形式化中的元建模和面向对象。SIMTHESys是一个多形式主义框架，用于定义新的形式主义和生成相关的求解器，基于对元素行为和行为接口的描述，以集成元素，E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）6175解算器。在大多数这些方法中，支持模块化或组合性，并且在某些情况下利用它们来增强解决方案过程。在SHARPE中，模块通过其源代码进行现代化管理;在Müobius中，复杂模型组合策略允许优化解决方案;在OsMoSys中，组合模型通过工作流程中不同子模型的不同求解器的编排来解决[14]。在其他情况下，建模者没有明确使用多元形式主义和/或模块化，而是用于优化分析（例如[22]）：一般来说，模块化表明部分解决方案的可能性，如果某些假设得到验证，这是可能解决方案的过程可以基于翻译到一个单一的解决方案形式主义，如在AToM3，并在某种程度上，莫比乌斯，或通过使用native求解器和组合形式主义，如OsMoSys，或通过两种技术的组合，如SIMTHESys。除了这些方法，情况是还注意到，同一模型可以在同一工具中用不同的求解器求解，称为多解范式。注意，通过还原到另一个可解形式主义的解决方案也广泛用于单一形式主义建模技术。这是一种广泛的方法，为建模者提供了非常抽象的规范机制，而无需手动生成不可管理的链。这种逻辑与本文的范围非常相关，因为产品形式解决方案的适用性将通过在SIMTHESys框架中实现一个真正的高级形式主义交互机制来实现，该机制可以映射到（产品形式）马尔可夫链上。4.2产品形态通过组合相互作用的子模型来定义随机模型在性能工程领域中起着重要的作用事实上，这允许人们解决现代系统的硬件和/或软件架构的复杂性。然而，一般来说，这些模型的稳态分析不利用它们的模定义，而是依赖于底层马尔可夫链的全局平衡方程系统的精确或近似解。乘积形式理论已被引入到嵌入网络领域，并在一系列条件下，允许通过隔离其组件来执行复杂模型的静态分析。一旦考虑到与模型的其余部分的相互作用而对每个部件进行参数化并求解，则关节模型的稳态分布被导出为孤立部件的分布的归一化乘积虽然乘积形式是为离散网络引入的，但它已经被各种形式主义所识别，如随机Petri网，随机自动机网络和马尔可夫过程代数。本文采用多智能体逆向复合智能体76E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）61定理（MARCAT）[18]来检查条件并导出多形式随机模型的乘积形式稳态分布。MAR-CAT是一个非常一般的结果，能够统一研究各种类型的乘积形式模型，包括Boucherie相对于其他结果，如拟可逆性和反向复合代理定理（RCAT）[17]，MARCAT更一般，但它需要分析模型的联合状态空间的遍历部分乘积形式定理的普遍性引起了一些问题，这些问题在关于乘积形式嵌入网的开创性著作中没有得到解决。特别地，部件的参数化的计算这个问题与RCAT的一般性有关，已经在[21]中得到了解决，其中给出了一种迭代算法（INAP），从随机自动机的定义开始，有效地计算正确组件在本文中，我们已经扩展了INAP的实现，以encom-pass MARCAT乘积形式，因此检查联合状态空间上的方程，并开发了一个接口，允许SIMTHESys的多形式主义工具应用INAP，以有效地决定模型是否允许MARCAT乘积形式的解决方案，并在假定答案的情况下计算它。关于随机自动机网络和产品形式，这个主题已经在几个作品中得到了解决，例如[10，12]。然而，我们工作的主题是相当不同的：而不是利用张量代数和产品形式之间的关系，使用SAN作为工具来表达动态的合作模型，我们有兴趣探索产品形式之间的在我们的方法中，SAN类结构已主要用作交换格式接口的模型分析工具与底层的解决引擎。5结论和今后的工作在本文中，我们提出了一种技术，以确定产品形式的解决方案，在一个多形式主义的框架。在生成状态空间的过程中，对解的存在性和计算性进行了检验构成研究中的主模型的子模型。 状态空间是使用与形式主义规范相关联的行为生成的。这提供了更大的灵活性，并允许将产品形式解决方案应用于新的形式主义，而无需开发新的工具。未来的工作将包括研究更复杂的同步机制，E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）6177anisms，并使用产品形式的解决方案，以接近真正的解决方案时，不尊重必要的条件引用[1] Balsamo，S.，G. Dei Rossi和A. Marin，一种用于乘积形式的协作马尔可夫链的数值解的工具，在：Proc。311-324.[2] Balsamo，S.，P. G. Harrison和A. Marin，A unifiable approach to product-forms in networkswith finite capacity constraints，in：Proc. of the 2010 ACM SIGMETRICS Int. Conf. onMeasurement and Modeling of Computer Systems，New York，NY，USA，2010，pp. 25比36[3] Balsamo，S.，P. G. Harrison和A. Marin，Methodological Construction of Product-FormStochastic Petri-Nets for Performance Evaluation ， J. of System and Software85（2012），pp. 1520-1539年。[4] Barbierato，E.，M. Gribaudo和M.Iacono，使用SIMTHESys定义绩效评估的形式主义，电子。注意Theor。Comput. Sci. 275（2011），pp.37比51[5] Barbierato，E.，M. Gribaudo和M. Iacono，在SIMTHESys中利用多形式主义模型进行测试和性能评估，在：第五届国际ICST性能评估方法和工具，VALUETOOLS121-130[6] Barbierato，E.，M.格里包多湾Iacono和S. Marrone，Performability modeling of exceptions-aware systems in multiformalism tools，in：Proceedings of the 18th international conferenceonAnalytical and stochastic modeling techniques and applications，ASMTA257[7] 博斯，F.， P. Buchholz和P. Kemper，用于deds的功能和定量分析的工具箱，在：第10届计算机性能评估国际会议论文集：建模技术和工具，TOOLS356-359.[8] 布舍里河J.，竞争马尔可夫链的独立性特征及其在随机Petri网。软件工程20（1994），pp.536-544.[9] 恰尔多湾和A.S. Miner，Smart：The stochastic model checking analyzer for reliabilityand timing ， Quantitative Evaluation of Systems ， International Conference on0 （ 2004 ） ，pp.338-339。[10] DaoThi ， T.H.andJ.M.Fourneau ， Stochasticautomatanetworkswithmaster/slavesynchronization ： Product form and tensor ， in ： Proceedings of the 16thInternationalConferenceonAnalyticalandStochasticModelingTechniquesandApplications，ASMTA279-293.[11] de Lara，J.和H. Vangheluwe，Atom3：一个多形式主义和元建模的工具。，在：R.- D.Kutsche和H. Weber，editors，FASE，Lecture Notes in Computer Science（2002），pp. 174-188.[12] Fourneau，J.M.，B. Plateau和W. J. Stewart，无同步的随机自动机网络中乘积形式的代数条件，执行。评估，Elsevier65（2008），pp. 854-868[13] Franceschinis，G.，M.格里包多湾Iacono，S. Marrone，N. Mazzocca和V. Vittorini，复杂系统的组合建模在ICATPN'04中的联络中心场景，2004年，第10177-196.[14] Franceschinis，G.，M.格里包多湾Iacono，S. Marrone，F. Moscato和V.Vittorini，基于组件的形式化模型开发中的接口和绑定，在：Proc。 第四届ICST国际绩效评估方法和工具会议，VALUETOOLS '09（2009年），第100页。44：1-44：10。[15] Gelenbe，E.，产品形成网络与消极和积极的客户，J。的Appl.概率28（1991），pp. 656-66378E. Barbierato et al. /Electronic Notes in Theoretical Computer Science 296（2013）61[16] Gelenbe，E.，G-网络与触发的客户运动，J.应用概率30（1993年），pp. 742-748[17] Harrison，P.G.，Markovian process algebra，理论计算机科学290（2003），pp. 1947-1986年。[18] Harrison，P. G.和T. T. Lee，Separable equilibrium state probabilities via time reversal inMarkovian process algebra，Theoretical Computer Science346（2005），pp. 161-182.[19] 亚科诺，M.，E. Barbierato和M. Gribaudo，SIMTHESys多形式主义建模框架，计算机和数学与应用（2012）。[2