UML 2.0活动图数据流语义验证及其形式化分析

理论计算机科学电子笔记127（2005）35-52www.elsevier.com/locate/entcsUML 2.0活动中数据流的语义与验证HaraldStoürrle1德国慕尼黑大学信息学院摘要从UML 1.5到UML 2.0的一个主要变化是活动图的再工程。这篇文章检查了在当前版本的UML中描述的活动模型2.0通过定义指称语义来实现标准。它涵盖了基本的控制流和数据流，但不包括层次结构，扩展节点和异常处理（参见[18，19，20]这些问题）。该文件显示，在标准中提出的结构不那么容易形式化，以及如何形式化可用于形式化分析。关键词：UML 2.0、活动图、数据流、Web服务建模、工作流和面向服务的体系结构1介绍1.1动机和目标业务流程和工作流程的建模是软件工程中的一个重要领域活动图被引入UML的时间相当晚。它们主要被认为是一种工作流定义语言，但在对Web服务进行建模时，它也是自然的选择，并在指定系统级行为方面发挥着重要作用。UML已经成为1电子邮件地址：stoerrle@pst.ifi.lmu.de1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.04636H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）35到2.0版），包括对活动的完整重新定义。不幸的是，该标准又一次未能定义一个正式的语义，这对于充分利用UML是必要的，例如，自动化工具。与UML1.5相比，活动图的具体语法在控制流程方面基本相同。然而，其他一切都发生了巨大的变化。这些变化包括了数据流的具体语法，所有的抽象语法 ， 特 别 是 语 义 ： 虽 然 在 UML 1.5 中 ， 活 动 图 被 定 义 为 一 种 状 态 机 图（ActivityGraph曾经是Meta模型中StateMachine的子类），但现在两者之间没有这样的联系：“在UML 1.5中，活动取代了ActivityGraph。“（比照[15，第292页]）。该标准声称[15，第292页]）。本文试图找出Petri网实际上可以在多大程度上用于这一目的。1.2方法为了找到答案，我们研究了标准，并试图用Petri网定义一个形式化的语义。然而，传统的P/T网不适合于这项任务，因为活动图也具有过程调用和数据流功能。虽然过程调用的问题已经在[18]中使用过程Petri网系统的概念进行了解决（参见。[12]），本文转向数据流问题。有几个扩展的基本Petri网模型，能够建模数据流。这些通常被归入“高阶网”的标题下（参见。[11]），其中[10，9]可能是最知名的。1.3相关工作在撰写本文时，UML 2.0的工作已经达到了最终化阶段。据说技术工作已经结束，投票应该在今年晚些时候完成，导致对新的UML版本的官方认可可能在2005年初。因此，目前可用的规范[15]已经非常接近今年晚些时候（或明年初）将成为UML 2.0的规范在UML 2.0中，相对于UML 1.5有许多实质性的改进。元模型已经完全重新设计，现在比以前更干净，更完整和正交。许多细节都得到了改进，UML2.0现在又以某种有意义的方式面向对象在外部，添加了一些新的符号元素，但最重要的创新是，符号元素现在可以与比以前少得多的限制相H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）3537然而，在语义方面，UML仍然不能令人满意。虽然许多问题已经被删除或解决，并且某些方面的描述更加清晰，但仍然没有正式的语义。在许多情况下，甚至没有足够的例子，例如，活动中的例外和交互中的否定，仅举两例。转向科学世界，似乎到目前为止，很少有关于活动图（无论版本如何）中的数据流和UML 2中的活动图的关于UML 1.x活动中的数据流[1]似乎是唯一的参考。关于UML2活动图，[2]非常简单地检查了引脚的语义。此外，还有C的一系列文章。Bock on UML 2 Activities，其中之一处理数据流[3]。虽然这些条款比标准更明确和完整，但缺乏形式上的精确性。由于作者参与了OMG在我以前的出版物中可以找到一种关于UML 2活动的更正式的方法：[18]处理控制流和过程调用，[19]处理异常，[20]处理扩展区域和结构化节点。这些论文还包括对文献的广泛调查也只有很少的贡献处理活动图的形式分析过程（当然没有数据流）。Li等人[13]展示了如何为活动指定持续时间约束。它们还提供了一种基于线性规划的验证算法。Rodrigues [17]建议使用有限状态过程，并且似乎有一些工具支持它们的形式化分析，但没有提供任何细节。最后，[6，7，8]提供了一个从活动图的限制类到标记转移系统的映射，并详细说明了时间逻辑（CTL）公式的验证和静态结构约简规则，如Petri网所知2UML 2.0在本节中，我们讨论UML 2.0中的活动，特别强调对UML 1.x的区别。活动图最好通过一个例子来解释（见图1，改编自[15，图203，第290页]）。该示例由两个图组成，一个类图（左）和一个活动图（右）。请注意，Order类有第三个隔间，其中包含对活动图OrderBehavior的引用。这样，类图就为活动图设置了必要的上下文，为我们提供了活动图的题字语言（有关上下文的更多信息，请参见2.2节38H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）35订单示例CD秩序填充：布尔billed：Boolpaid：Boolshipped：Boolgoods：Goodsame（Order）：Boolinit（Int）：Orderjoin（Order，Order）：Order pay（）：void订单行为{reject}接收订单[接受]填充有序{fill= true}生产商品发送发票接收运送货物支付{pay（）}关闭订单ADFig. 1.一个介绍性的规范，由一个类图（左）和一个活动图（右）组成。Order类的第三个隔间中的图标是对图OrderBehavior中指定的Activity的引用。关于活动图，预期有以下行为。首先，通过动作接收命令来接收命令。菱形表示决策节点。在第一个分支上带有方括号的表达式断言，如果该分支被采用，则上下文处于接受状态。注意，像这样的保护可以但不需要对应于上下文的属性。接下来，执行actionfill命令，调用花括号中的行为，并到达fork（第一个黑条）。分叉将控制流的路径一分为二。2在左边的路径上，操作生产货物和运输货物已执行。在正确的路径上，操作send invoice和receive付款已执行。收到付款后，调用行为pay（）。这两条道路是并行的。当它们都完成执行时，连接（另一个黑条）可能发生，并且操作关闭顺序被执行。返回到上面的决策节点（在接收订单之后），它的第二个分支调用行为reject。请注意，此行为不是由上下文指定的。一般来说，这只是一个直观的例子，而不是一个完整的例子：模型编译器可能会拒绝它，或者至少警告用户系统[2]目前的标准定义了这里的数据令牌会发生什么H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）3539类型{expr}[guard]类型{expr}[guard]类型{expr}[guard]类型{expr}[防护]效果类型{expr}[警卫]被低估了。也可以说，问题应该以不同的方式建模，但为了讨论起见，我将坚持这个例子，因为它是贯穿标准本身的一个例子这个例子超越了UML标准，因为每个图都被放入一个表示其类型和名称的框架中，而标准只为交互图定义了这一点。然而，这是一种良好的做法，在指定系统时应遵循。注意，只有这个特性允许我们在自己的一个digram中单独指定OrderBehavior，并从Order的第三个隔间中引用它。UML标准中提出的过程要求我们绘制整个Activity（而且只有一个！）在第三个隔间。2.1具体语法活动图的具体语法在控制流程方面只有轻微的变化，但在数据流程方面有一些有趣的（和有问题的）差异。一个值得注意的扩展是泳道现在提供的灵活性，它接近于模拟UML中的一种用例图2.0（参见[4]）。然而，它并不影响Activity的行为，因此在此可以忽略。次级活动状态已经消失，嵌套现在通过从定义高级活动行为的Action调用次级活动来完成。数据流现在由ObjectNodes和ObjectFlows表示。该标准允许数据流使用三种不同的符号（参见图2）。首先，有一个类似于UML 1.5的符号，其中数据流被显式指定。UML 2.0中唯一的区别是虚线箭头被实线箭头所取代图二.数据流的具体语法：UML 1.5表示法（左），以及替代的等效UML2.0表示法（所有其他），包括其次，有一个简化的版本，允许附加数据流 项到控件的窗口边缘，就视觉表示而言这{expr}[guard]40H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）35从实用的角度来看，这种表示法特别方便，因为使用这种表示法，首先很容易指定控制流，然后稍后有选择地添加数据流，而不改变控制流。事实上，UML的许多其他部分也有类似的过程，甚至可以将其视为增量方法的基础但并不完全清楚这个符号的真正含义。可能有两种解释。 首先，将一个ObjectNode“附加”到一个现有的ActivityEdge可以被解释为引入ObjectNode和两个ObjectFlow（ObjectFlow没有可视化地表示）。其次，它可以被解释为引入ObjectNode，并将一个ActivityEdge替换为两个ObjectFlow。 第一种解释似乎更接近直觉，特别是上面提到的创建活动图的增量方法。另一方面，第二种解释将避免“看不见的”弧线。然而，这两种解释都只影响具体句法向抽象句法的过渡，而不影响抽象句法向语义的过渡。但是，我们必须要求图表是完整的，也就是说，没有遗漏。 特别是，只有那些实际存在于Activity中的ObjectNode和ObjectFlow才被翻译。在实际环境中，人们很少会填写活动图的所有细节，但期望人类理解直觉。图1就是一个例子：人类读者会简单地掩盖不完整和草率的注释。然而，对于形式语义学来说，这是不能容忍的。因此，出于本文的目的，我们假设没有省略任何元素。此外，为了简单起见，我们假设活动图中使用的操作被指定为类的方法。因此，完整和正确的示例如图3所示。在这里，拒绝的结果被省略了，因为它代表了人类的决定，我们选择不在我们的模型中实现这些结果：我们将能够在模拟网络时做出这个决定。出于同样的原因，接受的警卫已经走了。该标准并没有指定一个具体的语言来描述铭文，包括守卫、对象节点上的引用等等。同样，计时注释也没有定义。 事实上，没有一个具体语法的例子，并且对“动作语义学”的引用很少。所以，我们或多或少得创造一种铭文语言。它相当简单，接近SML。有关详细信息，请参阅数据流部分。标 准 中 还 提 出 了 第 三 种 数 据 流 表 示 法 （ 再 次 参 见 图 2 ） ， 它 将 Pin（ObjectNode的子类）指定为这样做的目的H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）3541订单示例CDB一C一BC秩序填充：布尔billed：Boolpaid：Boolshipped：Boolgoods：Goodreject（）：voidaccept（）：voidsame（Order）：Boolfill（）：voidbill（）：void pay（）：voidship（）：void init订单行为接收订单{o.init（）} o.Ordero：订单o：订单填充有序o：订单{o.fill（）}秩序运送货物o：订单发送发票o：订o：订单接收{o.bill（）}{o.ship（）}支付[o.id =o'.id]o '：订单{o'.pay（）}排序{join（o，o '）}{o.close（）}o：订单秩序关闭订单AD图三. 图1中活动图的一个更详细的版本。符号在过程调用的上下文中变得更容易理解，参见图4。见图4。 Pin是用于细化的ObjectNode。2.2抽象语法活动的元模型在UML 2.0中已经从头开始重新设计。活动图的主要概念现在称为活动，42H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）35*呼叫输入输出目标源*ExecutableNode行动ActivityNode* **1 1活动优势活动⟨⟩控制节点ObjectNodeExecutableNodeActivityNodeActivityNode合并节点“替换了UML 1.5中的ActivityGraph。“（比照[15，第292页]）。Activity不再是StateMachine的子类，而是“重新设计为使用类似Petri的语义而不是状态机”。“（比照[15，第292页]）。 元模型定义了六个层次的表达能力。第一级（ForkNodeJoinNode图五. UML 2.0元模型的一小部分：活动要么有动作，要么有ActivityNodes和ActivityEdges的图（左）;节点和边的种类（右）。ObjectFlow.e对象是ObjectFlow. e对象类型枚举（创建、读取、更新、删除）的元素基本的两个实体是操作和活动。虽然“行动”是可执行功能的基本单元“（参见， [15，第280页]），一个活动提供了[15，第280页]）。这种协调被捕获为由ActivityEdges连接的ActivityNode的图（参见图5）。数据流使用ObjectNodes和ObjectFlows表示，它们分别是ActivityNodes和ActivityEdges的子类。 有关活动图的元模型部分，请参见图5对于Meta类的所有实例，通常的点表示法用于访问实例的字段，即，要提取给定ObjectNode的状态o，我们写o。in State等等。为了方便起见，我们假设活动在数学意义上表示为图，即，形式为ActivityNodes、ActivityEdges，其中ActivityNodes和活动优势是再次分区到各自的元类中。也就是说，ActivityNodes实际上是一个元组再一次地，N，N，BN，CN，ON，其中：EN可执行节点的集合（即基本动作）;类型：分类器TypedElement警卫队活动优势DecisionNode初始节点FinalNode0..10..ObjectNodeinState：StateupperBound：ValSpecObjectFlow转换：行为选择：行为效果：{C，R，U，D}H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）3543iN、fN初始节点和最终节点（其中每个节点可能只有一个）;BN是分支节点的集合，包括MergeNodes和Decision-Node;CN并发节点的集合，包括ForkNode和JoinNode;在ObjectNode的集合而ActivityEdges是一对函数，其中：AE可执行节点和控制节点之间的普通ActivityEdges集合;一方面是ExecutableNodes和ControlNodes之间的ObjectFlow集合，另一方面是ObjectNodes之间的ObjectFlow集合从现在开始，我们将使用Activity的这种抽象语法表示3数据流语义在新的UML版本中，活动现在“使用类似Petri的语义而不是状态机。“（比照[15，第263页]）。 我们现在将尝试通过定义活动的形式语义来检查这一点。为了保持这种语义的简单性，我们对具体语法施加了一些限制。因此，假设合并控制流总是由MergeNode正确建模（参见图3）。这里忽略过程调用-[18]中的处理是正交的，因此可以随意添加。此外，还省略了连接器以及发送、接收和时间事件。我们要求，在活动中有唯一的初始和最终节点。我们要求所有元素都使用全局唯一的名称命名。关于数据流，只使用了一种表示法（ObjectFlows附加到ActivityEdges的表示法，参见图2所示的第三种变体）。所有其他的符号都被认为是语法加糖。然而，请注意，对于初始和最终节点，传统的符号是必要的，并且带有附加ObjectNode符号的弧实际上表示两个ObjectFlow和一个ObjectNode。然后，只有那些实际存在于Activity中的ObjectNode和ObjectFlow才被翻译（参见。见图3）。人类观察者可能在他的头脑中添加的隐含元素不会被翻译。3.1语义域活动的数据流设施可以由高级Petri网表示（参见. [11、10、9]）。出于务实的原因--良好的工具支持的可用性，44H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）35→→我的天| {\fn方正粗倩简体\fs12\b1\bord1\shad1\3cH2F2F2F}名称，但这里选择单色Petri网（CPN）作为语义域（参见图7中的示例）。定义3.1（有色Petri网的有色Petri网（CPN）是一个元组，其中包含：N是一个由位置、变迁和弧组成的Petri网P，T，A; SigAlg是一个由排序和运算组成的Petri-代数Pcolor是一个全函数P→N，为每个位置分配一个排序（“color”）;guard是一个全函数T Expr，为每个位置分配一个布尔表达式。transition，默认为常量tt;eExect 是一个总函数AExpr，它为每个弧分配一个表达式，其类型是弧的位置的颜色。为方便起见，颜色、保护和效果可能会部分指定，默认为黑点标记。 也就是说，如果color（p）是unfined，那么color（p）=TOKEN是有意的，guard和eclect的默认值分别是true和skip网络系统行为的定义稍微复杂一点，因为我们现在需要考虑令牌的值和含义。 对他们的操作。 CPN的标记是一个多集（或词），p，v p P，vcolor（p）. 由于我们缺乏完整定义的空间，我们只能在这里提供一个示例：考虑图8的示例运行，图7的网络，表示图3的活动图。注意，CPNs的网元与过程Petri网的网元是正交的。因此，这里定义的数据流的语义可以与[18]中定义的过程调用语义3.2语义映射在本节中，我们首先概述语义映射背后的直觉，然后提供一个精确的定义。关于控制流，Ex-ecutableNode成为网络转换，ControlNode成为网络位置或小网络片段，ActivityEdges成为网络弧，可能具有辅助转换或位置。对于数据流，ObjectNode成为网络位置，ObjectFlow成为网络弧。请参见图6以直观地了解翻译过程。在这一点上，我们还需要处理ObjectNode和ObjectFlow上的铭文。UML标准在其语言方面相当不具体。现在我们通过检查UML标准提供的示例来澄清对铭文语言的要求（参见见图3）。H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）3545可执行节点UML AD活动petri网活动活动优势以下情况除外：除非：UML ADpetri网辅助控制节点fork/joinObjectNode类型类型ObjectFlowsexprexpr图六、活动的控制和数据流的语义映射的直观性在这个例子中，基本上有四种铭文。 首先，在ObjectNode上有类型声明（在我们的解释中，它们成为相应CPN位置的颜色）。某些ObjectNode还声明了一个变量（在示例中称为o），表示驻留在ObjectNode中的类型的实例。在与ActivityNode相邻的ObjectFlows上声明的一组变量构成了ActivityNode执行的Action的名称空间（假设它是一个ExecutableNode）。其次，ActivityEdges上的花括号中有选择、选择和转换函数。 我们所能合理了解的是，它们在给定的命名空间上工作，改变某些对象的状态在其中，可能增加或减少名称空间。 建模者必须填充细节，效应表达式通过转换简单地传递下来，并映射到连接到表示ActivityEdge的过渡的弧的效应表达式。在我们的解释中，这些功能保持在各自的净弧。第三，在ActivityEdges的方括号中有保护函数。它们只是访问命名空间，并可能读取其中对象的状态。在我们的解释中，它们被向上或向下移动到下一个净转换。同样，确切的含义留给建模者，表达式被转换为守卫（封闭的布尔表达式），这些守卫由与表示ActivityEdge的过渡相邻的弧定义考虑到这些需求，我们采用了CPN工具集中使用的铭文语言（参见[5]），这是标准ML的方言[16]。这样，就确保了对案例研究和分析技术的工具支持。作为一个例子，请重新考虑图3中的Activity，并将其转换为46H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）35⟨⟩CPN如图7所示（该图是从CPN工具集打印出来的）。图7中网络左上角的文本是CPN工具集中定义铭文的标准ML代码：E是传统黑点标记的类型，而ORDER是一个自定义的类型，携带订单的状态。网络是使用CPN工具集手动创建的，并且完全可以运行（参见图9的屏幕截图）。形式语义也相当简单。我们必须通过函数[ ]]将Activity_ActivityNodes，ActivityEdges_ 的 抽 象 语 法 表 示 映 射 到 CPN_N ， SigAlg ， color ， guard ，e_ectors_，其中N = P，T，A，并且ActivityNodes和ActivityEdges被划分为各种节点和边，如上所述。语义函数[]的定义如下：P={iN，fN}BNON{pe|e ∈ AE，{e. 源，E。目标} ENCN}，T= ENCN{te|e∈AE，{e. 塔吉特角源}BN{iN，fN}}，A={e.source，xe，xe，e. 目标函数|e ∈ AE，xe∈ P<$T}{|<$x，y<$∈AE<$（x∈P，y∈T）<$（x∈T，y∈P）}SigAlg = 0. 类型|o∈ON}，{a. 转型|a∈OF}颜色={o} → o。类型|o ∈ ON}检查={a} →a. 转型|a∈OF}警卫队 ={t›→a，t选择权A，a，b，a，选择|a∈OF}。观察点符号的使用以访问与边缘相邻的节点（参见图1）。见图5）。如果o.upperBound被定义为一个ObjectNodeo，这可以被解释为使用规范构造的相应位置的容量4数据流分析有了上一节定义的语义，我们现在可以将所有用于验证和确认Petri网的标准技术转移到UML2.0活动图 在本节的其余部分，我们假设A是通过上述语义映射到CPNN的活动（即，[[A]] =N）。我们假设N存在对应于A的初始和最终状态的可感知的初始和最终标记。H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）3547在ID接收命令加入1`1（id，false，false，false，false）P1秩序秩序INT命令填充顺序颜色顺序=产品INT * BOOL * BOOL * BOOL * BOOL;var id：INT;var order，order2：ORDER;fun init（）=（1，false，false，false，false）;fun fill（o1：ORDER）：ORDER =（#1 o1，true，#3 o1，#4 o1，#5 o1）;Fun bill（o1：ORDER）：ORDER =（#1 o1，#2 o1，true，#4 o1，#5 o1）;fun pay（o1：ORDER）：ORDER =（#1 o1，#2 o1，#3 o1，true，#5 o1）;fun ship（o1：ORDER）：ORDER =（#1 o1，#2 o1，#3 o1，#4 o1，true）;秩序P3秩序秩序填写（订单）p2订单秩序秩序P5秩序秩序汇票（订单）P6秩序fun same（o1：ORDER，o2：ORDER）：BOOL=（#1 o1）=（#1 o2）;fun join（o1：ORDER，o2：ORDER）：ORDER=（#1 o1，#2 o1或#2 o2，#3 o1或#3 o2，#4 o1或#4 o2，#5 o1 orelse #5 o2）;船舶（订单）P4秩序[ same（order，order2）]秩序支付（订单）P7秩序秩序秩序order2join（order，order2）P8秩序秩序图7.第一次会议。表示Activity和图3中声明的类型的Petri网。4.1验证在测试或检查设计时，迹线可以提供很大的帮助。有了上面提供的CPN语义，这两种方法现在都可用于UML 2.0活动。通过抽象出“内部”操作aux、fork和join，可以将N的跟踪转换为A重新考虑图3中所示的活动，该活动已被转换为图7中的CPN。假设一个初始标记代表了InitialNode的位置，我们可以通过手动模拟（“令牌游戏”）、工具支持的交互式模拟或批处理计算来生成跟踪将CPN跟踪映射回Activity非常简单。 由于我们选择了带有标准ML铭文的CPN作为我们的语义域，我们可以使用CPN工具集作为#1订单fNINT闭序收到付款装运货物发送发票叉aux48H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）35模拟器 请参见图9，其中显示了CPN工具集执行图7中的net。[3]甚至可以将其用作活动图的可视化模拟的基础。4但是，生成跟踪需要初始标记，这在UML标准中是没有提供的。为了简单起见，我们只取一个值为1的token作为初始标记。在CPN工具集使用的铭文语言中，这个初始标记被写为标记从该标记开始的此步骤的变量绑定⟨接收订单id= 1p1，填充命令order=1，，，，p2，叉order=1，，，，3，3，3，3，3，3，3，4，4，5-四氢呋喃，2015年12月5日，2015年12月1日，2015年12月15日，2015年12月15日，2015年12月15日，2015年12月16日，2015年12月16日，2015年12月16日，发送发票运送货物order=101，tt，102，103，104order=101，tt，102，103，104第4，第1，第2，第3，第4，第5，第6，第7，2016- 06-2501：00：00收到付款order=1，tt，tt，n，n第4，第1，第2，第3，第4，第5，第6，第7，2017- 07-21 00：00：00加入order=1，tt，n，n，ttnorder2=101，tt，tt，tt，2008年8月，2001年，tt，tt，tt，tt，关闭订单id= 1身高1见图8。 图7中CPN的运行，表示图3中指定的活动（每行是一个步骤）。在这里，我们在位置iN处使用简化的初始标记4.2标准属性确定是否可以到达某些状态通常具有很大的实际价值。例如，问题可以形式化为m∈RN（m）：m∈RN（m），其中RN（m）表示从m可到达的N的标记的集合，并且m和m分别是N类似地，可以通过确保H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）3549不<$m∈RN（m）：<$t∈TN：m−→，3对于这个例子，从Activity到CPN的转换仍然是手动完成的，但我正在自动化这个过程。4CPN Toolset的前身最初是作为IDEF的模拟器而设计的50H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）35填充命令见图9。 使用Design Toolset对图7所示的网络进行模拟运行的两个屏幕截图：初始状态（左）和发送第一张发票后但为其发货前的状态（右）。其中m−→t是表示转换t被激活的Petri网符号inm.最后，像“如果订单完成，最终会运送相应的货物吗？”这样的属性可以用类似的方式表达mJ∈RN（m）：mJ−s−h−ip−g−o−o−ds−o−rd−e→r这些属性在结构上非常相似，因此将直观的属性转换为Petri网术语并为UML活动解释其结果是非常容易的。4.3定量分析在设计和分析业务流程、物流和制造问题等方面使用基于Petri网的工具的一个重要原因一直是可以进行模拟和应用定量分析技术。在这些情况下，验证订购的货物最终是否发货是不够的，但我们需要确保一定的时间范围。此外，对于许多应用程序，确定 在任何给定时间或平均时间驻留在系统中的订单，H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）3551确定系统处理给定负载所需的最小容量。这类问题经常被随机Petri网攻击，并且有大量的工作处理UML 1.x活动图中与性能相关的问题，而不是UML 2.0。不幸的是，该标准没有提供应用Petri网的典型分析技术所需的各种铭文，更不用说所需的概念框架了。因此，我们需要对UML活动图进行语法扩展，以涵盖诸如动作的持续时间、频率、概率和延迟等方面。虽然已经有许多方法来提供和利用UML 1.x的这种扩展（例如[13，21，14]），但还不清楚这些扩展是否以及如何转移到UML的新版本5结论本文定义了UML 2.0中活动图的形式化语义。它基于有色Petri网，涵盖了控制流、并发和数据流，但不包括过程调用、异常处理和扩展区域（参见[18，19，20]）。通过仔细选择网络形式主义和铭文语言，CPNs的标准分析技术和工具可以用于UML活动的验证和确认由于这里给出的语义在产生的Petri网中保留了原始活动图的结构，因此在活动和相应的Petri网之间进行映射非常容易，从而打开了在活动和相应的CPN之间进行简单映射的道路，甚至可视化活动的执行。这对于基于非图形形式主义的语义来说是非常困难的，如果不是不可能的话，比如进程代数。最后，定义语义也有助于识别标准中的一些缺点目前正在实施一种支持工业案例研究的工具，同时扩展分析技术并使之自动化然而，由于目前缺乏真正的UML 2.0工具，这一进展受到了阻碍：尽管许多供应商做出了市场承诺，但目前还没有这样的工具可用。随着UML 2.0标准的正式采用，我们希望这种不愉快的情况将会消失。下一步是扩展此语义，以涵盖处理时间和处理数据量等定量方面。此外，流数据的处理是一个未解决的问题。看看这些扩展是否允许在开发的早期阶段对系统架构进行定量分析是很有趣的在Petri网世界中，基于马尔可夫链的分析技术有着悠久的传统，因此将本文中提出的semantics转换为创建广义随机的semantics似乎是可行的52H. Störrle/Electronic Notes in Theoretical Computer Science 127（2005）35用Petri网代替有色Petri网。引用[1] Allweyer ， T.Loos ， ProcessOrientationinUMLthroughIntegrationofEvent-DrivenProcessChains，in：P. -A. Muller和J. B'ezivin，编辑，国际工作室UML '98：Beyond theNotation（英语：UML' 98：Beyond the Notation）（1998）183-193.[2] Barros，J. P. 和L. Gomes，ActionsasActivitiesasPetrinet s，in：J. 尤延斯湾Rump e，R. France和E. B. Fernandey，editors，Proc. Ws. Critical Systems Development with UML，2003，pp. 129比135[3] 博克角，UML 2活动和动作模型：对象节点，J.对象技术3（2004），pp. 27www.jot.fm[4] 布 尔 河 J.A. ， Use Case Maps as Architectural Entities for Complex Systems ， IEEETransactions on Software Engineering24（1998），pp.1131-1155.[5] CPN Tools Team，CPN Tools Manual，Technical report，Univ. of Aarhus（2004），可在http://wiki.daimi.au.dk/cpntools/cpntools.wiki网站。[6] Eshuis，H.，“语义和验证UML活动图的工作流程建模，”博士。thesis，CTIT，U.Twente（2002），作者[7] 埃舒伊斯河和R. Wieringa，UML活动图的形式化语义-工作流程模型的形式化，技术报告CTIT-01-04，U。特文特省计算机科学（2001）[8] 埃舒伊斯河和R.Wieringa，使用UML活动图对工作流程设计的验证支持，在：Proc.24th Intl。Conf.on Software Engineering（ICSE）（2002），pp. 166比176[9] Genrich，H.和K. Lautenbach，[10] 詹森，K.，着色Petri网基本概念、分析方法和实际应用。第一卷，[11] Jensen，K.和G. Rozenberg，“高级Petri网。《理论与应用》，[12] Kiehn，A.，“一种构造Petri 网的机制”，论文，TU Mu ？n？chen （1989），1989 年3月被批准为TU Mu？n？hen的技术报告TUM-I8902。[13] Li，X.，M. Cui，Y.裴，Z.Jianhua和Z.郭亮，UML活动图的时序分析，in：M. Gogolla和C. Kobryn，编辑，Proc.第四国际。Conf. on the Uni Fied ModelingLanguage（UML2001），number 2185 in LNCS（2001），pp. 62比75[14] Merseguer，J.和J. Campos，265-289。[15] OMG，OMG统一建模语言：上层结构（最终采用的规范，版本2.0，2003-08-02），技术报告，对象管理组（2003），可在www.omg.org上获得，于2003年11月11日下载。[16] 保尔森湖C.的方法，[17] 罗德里格斯河W.，Formalising UML Activity Diagrams Using Finite State Processes使用有限状态过程，在：G. Reggio，A.纳普湾，澳-地朗普湾Selic和R. Wieringa，editors，Proc. Intl. UML模型中的动态行为：语义问题。德国慕尼黑路德维希-马克西米利安大学技术报告编号0006F.Informatik，2000，pp. 92比98[18] Stéorle，H.， UML2.0活动中控制流的语义，见：P. 博托尼角洪德豪森，S. Levialdi和G. To