UML活动图和类图的并发事务框架逻辑

理论计算机科学电子札记95（2004）83-109www.elsevier.com/locate/entcsUML活动图和类图的并发事务框架逻辑Franklin Ramalhoa，1，2，Jacques Robinb，3和Ulrich Schiela，4aDepartamentodeSistemase Computac巴西大坎皮纳联邦大学b巴西累西腓联邦大学摘要我们提出并发事务框架逻辑（CTFL）作为一种语言，提供形式化的语义UML活动和类图。CTFL通过面向对象的类层次结构和对象定义术语扩展了一阶Horn逻辑，并使用了五个新的逻辑连接符，这些逻辑连接符声明性地捕获更新和事务的时间和并发约束。CTFL有重合性、可靠性和反驳性的完备证明和模型理论。CTFL允许使用单一语言(1)形式化地描述活动图和类图的语义，（2）使用定理证明验证基于这两个图的UML模型，（3）将模型实现为可执行的、面向对象的逻辑程序。关键词：UML语义，面向对象逻辑程序设计，并发事务逻辑，框架逻辑。1Curre ntlyatCenetrodeInforma′ticatUni versidadeFederaldePernambuco，Brazil. 这项研究得到了巴西联邦政府CNPq的资助2 电子邮件地址：franklin@dsc.ufcg.edu.br3电子邮件：jr@cin.ufpe.br4 电子邮件地址：ulrich@dsc.ufcg.edu.br1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.00784F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-1091介绍统一建模语言（UML）[18]提供了一个直观的，视觉上清晰的标准符号，用于指定和建模计算系统。UML规范和模型比它们的自然语言对应物更精确，更不模糊。它们在促进参与系统开发的所有参与者之间的通信方面有很大的作用。然而，当前的UML标准仅仅是半形式化的，因为它的语义仅仅是用自然语言定义的，而不是用一些严格的数学符号。这严重阻碍了在基于UML的系统工程过程中，为模型验证、行为代码生成和代码测试构建和使用自动化开发工具。 为了克服这个限制，最近提出了各种建议，为各种UML图提供形式化的语义[9，6，5，21，8，1，16，30]。这些专业人员在描述UML图所使用的形式语言和依赖于这些语言的工具所提供的开发任务自动化功能方面是非常不同的。然而，涉及活动图的提案有一个共同的趋势，即：• 只关注活动和状态图，孤立地，在类图（CD）和其他结构图提供的结构上下文之外;• 只提供操作语义，这通常被认为在实践中主要对CASE工具开发人员有帮助，公理语义更适合应用程序设计人员，指称语义更适合语言设计人员[10];• 依赖于结构贫乏的命令式或函数式形式语言，这些语言不能很好地适应大多数基于UML的开发过程中使用的结构丰富的面向对象范式;• 依赖于低级的、通常相当《双城之战》的形式语言[26]，这迫使分析师进入微小的算法细节，这些细节在实现之前应该是抽象的，或者完全通过使用声明式编程[27];• 依赖于几种语言的组合，通常一种语言用于形式化UML图结构，另一种语言用于形式化期望的时间属性，另一种语言用于使用这两种形式符号实现关于模型的CASE工具推理，并且通常还有一种不同的语言用于实现从UML模型开发的系统。因此，开发团队希望利用这些建议，将UML直观的可视化清晰度与UML的严谨性、健壮性和F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-10985形式方法的CASE工具自动化面临着陡峭的学习曲线以及建模阶段的显着开发时间开销。 考虑到上市时间是大多数实际开发项目中最关键的因素，需要其他方法来扩大正式的、基于UML的开发的适用范围。在本文中，我们提出了这样一种替代方法来提供正式的语义UML模型。 它完全基于一阶喇叭逻辑（FOHL）的非单调变体。虽然这种方法有可能提供整个UML的语义和CASE工具，在本文中，我们提出了一个建议，专注于由类图5上下文的活动图的正式语义。我们展示了并发事务框架逻辑（CTFL）[14][4]如何为活动图和类图提供正式的语义。CTFL是FOHL的两个正交但协同的扩展的直接集成• 框架逻辑（FL）是一种面向对象的扩展，用于处理具有继承层次的复杂• 并发事务逻辑（CTL），一个处理复杂行为建模的非单调扩展，包括并发逻辑数据库更新、事务、进程通信和临时执行约束。我们的方法是基于UML活动和类图的元素和CTFL的构造函数之间的映射通过这种映射，这些UML图被赋予了证明理论和模型理论的形式语义：它们映射到的CTFL程序的语义本文的其余部分组织如下。在第2节中，我们回顾了UML活动图和类图的主要元素，并在一个简单的示例模型上对它们进行了说明。在第3节中，我们回顾了CTFL的面向对象和非单调结构，并在同一个例子中说明了它们。在第4节中，我们提供了第2节中提出的元素和第3节中提出的结构之间的系统映射这种映射定义了我们的UML活动和类图形式语义建议。在第5节中，我们指出了与相关工作相比，我们的方法的主要困难和优势。在第6节中，我们回顾了本文的贡献，并概述了未来工作的方向。5我们在这里不涉及类图的全部复杂性，将这个主题留给单独的出版物。相反，我们关注的是类图的主要特性，这些特性与为活动图提供上下文相关。86F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-1092UML类和活动图UML是一种图形和文本语言，用于面向对象软件工程（OOSE）中的规范和建模。在OOSE中，关键的软件结构是类。 类是对具有相似结构、行为和关系的对象的封装的、通用的描述。图1中给出了一个说明性的类图示例。 它是在[ 31 ]中提出的Royal &Loyal（RL&）公司信息系统类图的扩展。利发为多家公司管理忠诚计划，为常客提供航空里程或折扣积分等多元化奖励 类图指定了每个类的签名，即用于表示类对象状态的属性及其类型约束，以及用于表示这些对象行为的方法及其输入参数和返回值类型约束。 例如，在图1中，Customer类为一个fidelity程序客户建模，该客户具有string类型的name和title属性、一个boolean属性isMale、一个date类型的dateOfBirth属性以及一个整数返回方法age（）。类图还指定了定义的类之间的关系有三种主要类型的关系：专门化关系，用于指定类继承属性和方法的层次结构;聚合和组合关系，用于从被视为部分的简单对象组装复杂对象;以及用于其他关系的通用关联这些关系可以用基数约束来标记，基数约束是关于它们两端所涉及的元素的数量。例如，在图1中，Earning和Burning交易被定义为一般Transaction类的子类，该类的每个成员都与CustomerCard类的一个成员相关联。类图没有指定的是封装在类的方法中的行为。 UML提供了各种其他的图表来说明这个问题。状态图本质上是一个表示状态机的图。建议使用它来指定由于调用单个对象的方法和其他对象的方法而在该对象的属性值中发生的更改。它指定了触发这种变化的条件以及由此产生的新值。 相反，活动图本质上是一个活动图，建 议 用它来表示在用例实现中涉及的几个对象的属性值中发生的状态变化[22]。用例是将系统的功能划分为一组不同的基本用法的需求图。它们描述了每种用法所涉及的参与者和目的。在严格的面向对象开发中，每个用例最终必须由某个类的一个方法实现。活动图也可以用来描述行为分解F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-10987Fig. 1. UML类图以及通过从各种其他类调用对象的方法来实现的复杂方法的控制流程[28]。尽管所有的UML图对于复杂的系统开发都是有用的和互补的，但是用例图、类图和活动图可以被看作是UML的最小核心，简单的面向对象系统可以用它们来规范和建模。这就是为什么我们选择活动图和类图作为我们研究简单实用的UML模型形式语义的初始焦点。图2中给出了一个说明性的活动图示例。它对LoyaltyAccount类的burn方法的实现进行建模，88F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-109图1的类图。该方法本身实现了R L系统需求文档中同名的用例。 活动图是一个图，其中节点是活动或控制结构，弧表示它们之间的转换。活动被分解为原子动作图二. UML活动图对图1的类图中LoyaltyAccount类的burn方法进行建模既不能分解也不能中断的状态，以及可以中断并进一步分解为子活动的活动状态。这样的分解就可以用另一个细粒度的活动图来表示，复杂的活动就可以用活动图的层次结构来建模，这些活动图通过活动状态相互连接。除了其名称之外，动作状态还可以包含它所执行的操作的指定。这种规范可以使用对象约束语言（OCL）精确地编写，OCL是一种文本注释语言，是UML标准的一部分，它以直观的语法结合了逻辑和算法的最基本结构[31]。在图2的活动图中，BurnServiceItem节点是活动状态的一个示例，其行为由另一个F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-10989活动图（见图3）。这个活动图的所有其他节点都是动作状态或控制构造的示例。活动状态还可以包括在进入状态之前立即执行的进入动作和在离开状态之后立即执行的退出动作（分别地）。的图三. BurnServiceItem活动状态的UML子活动图活动图的控制结构是：（1）if/merge对，表示到互斥线程的条件分支，（2）fork/join对，表示并发线程，以及（3）synch状态，表示线程间同步约束。 例如，在图2的图表中，CheckEnrolled操作节点下面的分支节点模拟了操作CheckCard或操作CancelBurning必须紧接着的情况。相反，图3中图表顶部的fork节点模拟CheckStockOfServiceItem和CheckPointsAvailability动作必须始终并发地跟随CheckCard动作的肯定完成在同一个图中，UpdateLoyaltyAccount动作模型上面的同步状态指定它的执行必须等待另一个并发线程中的CheckStockServiceItem的肯定转换弧可以由其发生触发从一个状态到下一个状态的转换的事件来标记，或者由保护来标记，即，，一个先决条件，90F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-109← ∧∧J∗ ∗∗必须进行验证才能实现过渡。事件和守卫都可以用OCL表达式精确建模。活动图还可以包括将其链接到相关类图的对象流对象流将操作或活动状态关联到类。一个传入的命令流指定动作期望作为输入参数的对象的类。一个简单的输出流指定了作为输出参数返回的对象的类带有side exections的输出流指定了其属性因action或Activity的执行而改变的对象的类哪些属性被修改（以及如何修改）可以用OCL表达式精确地例如，在图3中，两个对象流建模UpdateLoyaltyAccount操作将类ServiceItem和LoyaltyAccount的对象作为输入参数，第三个对象流建模LoyaltyAccount类的输入参数的points属性被该操作更改。3并发事务帧逻辑CTFL是FL和CTL的集成，是FOHL的两个正交扩展，是经典一阶逻辑的子集，其中所有公式都是蕴涵正规形式[23]，每个蕴涵中只有一个结论因此，一个FOHL公式（也称为逻辑程序）是一个隐含的普遍量化蕴涵的合取，每一个都是：• 一个形式为cp1的限定条款。。 pn.， 其中c，p1，.， pn是正文字;• 形式为c ← true的事实，其中c是一个肯定的文字-通常缩写为c ←。3.1帧逻辑（FL）FL用两类新的面向对象的逻辑项扩展了一阶Horn逻辑：类定义项和对象创建项。类定义项指定类的超类及其适当的属性填充器和方法返回类型约束，遵循语法模式：class：：superclass s[. attritypO pitypei，.，met hj（.， para mk，. ）typO pjtypej... ]FL中有四个类型操作符，它们在上面的模式中实例化了typOpn：=>、=>>、=>和=>>。前缀的存在或不存在区分了可继承和不可继承的类型约束，而>和>>后缀指示属性或方法是否单值或集值。F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-10991J∗∗∗∗− ∗− −−一个对象定义项创建一个类的新对象实例，并为其分配适当的属性和方法返回值，遵循语法模式：object：class s[. attriassignO p1valuei，.，met hj（.， para mk，. ）assignO pjvalue ej. ]有 四 个 赋 值 运 算 符 ， 它 们 在 上 面 的 模 式 中 实 例 化 了assignOpn：>，>>，>和>>。 它们遵循与类型操作符相同的前缀和后缀约定在FL中，方法不像命令式面向对象语言一样有体。当一个方法的返回结果逻辑变量在定理证明过程中与一个值一致时，该方法被因此，属性和方法之间唯一的区别是方法可以带参数。FL类定义和对象创建术语被称为F分子。逻辑变量可以出现在这些分子中的任何位置：如对象名、类名、属性名、方法名、属性值、方法值或方法参数。这种自由为FL提供了一种高阶语法，允许非常简洁的元级规范。然而，存在从任何F-分子到FOHL文字的合取的简单易行的映射，这保证了在语义上，FL仍然是一阶逻辑[32]。为了更具体地说明FL，图4显示了表示图1的RL类图的FL事实。事实3和10将忠诚度Account和transaction定义为顶级类。在这些事实中，：模式的超类元素被简单地忽略了。 事实11和12定义烧和赚作为交易的两个子类。 这四个事实还定义了这些类的属性上的类型签名约束，例如loyaltyAccount类中的points=>integer，以及它们的方法参数和返回值上的类型签名约束，例如burn（integer，serviceItem）=>void。这些FL事实还通过属性定义了关联，这些属性的类型被约束到图的其他类，例如在事务类的定义中的card =>customerCard。92F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-109------• 事实1：customer[name *=>string，title *=>string，isMale*=>void，dateOfBirth *=>date，cards *=customerCard，programs *=loyaltyProgram，memberships *= membership，age（）*=> integer] ←.• 事实2：customerCard[valid *=> void，validFrom *=> date，goodThru *=>date，color *=>silver; gold，printedName *=>string，owner *=>customer，membership *=>membership，交易 *=transaction，checkCard（customerCard）*=> void] ←.• 事实3：loyaltyAccount[points *=>integer，membership*=>membership，transactions *= transaction，earn（integer）*=>void，burn（integer，serviceItem）*=> void，updateLoyaltyAccount（serviceItem，loyaltyAccount）*=> void，cancelBurning（）*=> void，completeBurning（serviceItem）*=>void，burnServiceItem（serviceItem，loyaltyAccount）*=> void，checkPointsAvailability（serviceItem，loyaltyAccount）*=> void]←.• 事实4：loyaltyProgram[customers *= customer，memberships *=membership，serviceLevel（integer）*=>> serviceLevel，partners *=programPartner，enroll（customer）*=> void，checkEnrolled（customer）*=> void] ←。• 事实5：membership[loyaltyAccount*=>loyaltyAccount，actualLevel *=> serviceLevel，card *=>customerCard，program *=> loyaltyProgram，customer *=> customer] ←.• 事实6：programPartner[numberOfCustomers*=> integer，忠诚度计划 *=loyaltyProgram，deliveredServices *=服务]←.• 事实7：service[condition *=> void，pointsEarned *=>integer，pointsBurned *=> integer，description *=>string，programPartner *=> programPartner，serviceLevel *=> serviceLevel，serviceItem *=serviceItem，transactions *=transaction] ←.• 事实8：serviceLevel[name *=> string，loyaltyProgram *=>loyaltyprogram，membership *=membership，availableServices*=service] ←。• 事实9：serviceItem[option *=>supermarket; fly; gas，points *=>integer，name *=>string，quantity *=>integer，updateServiceItem（serviceItem）*=> void，checkStockOfServiceItem（serviceItem）*=> void] ←.• 事实10：transaction[points *=> integer，date *=> date，status *=>inProgress; cancelled; completed，card *=>customerCard，loyaltyAccount *=>loyaltyAccount，service*=> service] ←.• 事实11：burning：：transaction[]←.• 事实12：earning：：transaction[]←.图四、CTFL事实库给出形式语义并实现图1的CD给出了FL的一对证明和模型理论[13]。证据是-该理论包括一个isaReflexivity公理，三个FOHL的等价、归结、因式分解和调节推理规则 ， 以 及 九 个 新 的 面 向 对 象 语 义 推 理 规 则 ： isaTransitivity ，F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-10993isaAcyclicity，94F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-109Ⓢ|⊗|⊕⊗∧subclassInclusion 、 typeInheritance 、 inputRestriction 、 outputRestriction 、scalarity、merging和elimination。模型理论由F-分子宇宙上的Herbrand模型组成。 在同一篇论文中，这两个语义都得到了证明是巧合的，健全的和反驳完整的。3.2并发事务逻辑顺序事务逻辑（STL）扩展了FOHL，增加了两个新的事务连接词：n元串行合取词和n元串行析取词。并发事务逻辑（CTL）进一步扩展了STL，增加了n元并发合取、n元并发析取和一元原子模态。这五个连接词允许以纯粹的声明和逻辑方式表示逻辑证明步骤的执行顺序的它们为逻辑程序、数据库更新和事务以及多代理和进程间通信协议提供这些新的连接词的语义是基于逻辑编程的执行概念作为证明尝试：• 串行连接p q的语义是：首先执行p;然后，如果p的执行成功（即，，如果它被证明为真），则执行q;如果两次执行中的任何一次失败，则p执行 q;如果它们都成功，则p执行q我的天• 序列析取的语义p q是p q的否定：首先执行p，然后不管结果如何，执行q;如果两个执行中的任何一个成功，那么p q也成功;如果它们都失败，那么pq也成功。• 并发连接词p的语义|q是：同时执行p和q。如果两次执行中的任何一次失败，那么p也会失败。|Q.如果他们都成功了，那么p也成功了。|Q.• 并发析取p q的语义是p q的否定：并发执行p和q;如果两个执行中的任何一个成功，p q也成功;如果它们都失败，pq也失败。• 在此上下文中，经典连词p q的语义变为：执行p和q，可以同时执行，也可以以任意顺序执行;如果两者都成功，则执行pq;如果其中一个失败，则执行pq。• 类似地，经典析取pq的语义仍然是经典合取p q的否定：同时执行p和q，或者以任何顺序依次执行;如果两者都失败，p q也执行;如果其中一个成功，p q也执行。F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-10995ⓈⓈ}{Ⓢ⊗这些顺序合取和并发合取（分别为析取）的真值表与经典合取（分别为析取）的真值表相同。这些新的连接词与它们的经典对应词之间的区别仅在于它们的执行顺序约束：对于“”和“”，它们是指定的和顺序的，对于“”和“”，它们是并发的。|“不，不。因此，|，，和是可交换的，和不是。原子模态连接符，防止其范围内的公式被部分执行。如果作用域为的原子连接的一个元素失败，或者其执行被某个事件中断，则必须回滚其他元素，并且必须还原所有已更改的对象在原子合取执行开始之前，它们的状态。例如，如果q在公式（p q）中失败，则必须回滚执行p所TL的一个关键特征是它刻意专注于从简单的行为和交易中定义复杂的行为和交易。它本身不包括任何原子更改或同步原语。为了在实践中使用，它必须用一组这样的原语进行参数化对我们的目的有用的原子变化对我们的目的有用的同步原语是跨多个线程共享的通道发送和接收同步消息因此，CTL（insert（Fact），delete（Fact），send（Channel，Fact），receive（Channel，Fact））为非单调FOHL和具有并发更新和事务的数据库提供了完全声明性的形式语义文[3]给出了STL的一对重合、可靠和反驳的完全证明和模型定理给出了它们各自对CTL的扩展在[4]中。该模型理论基于一种多路径结构，该结构捕捉了逻辑数据库在复杂事务应用于它时可能经历的状态，这些事务使用CTL的经典连接词和事务连接词来组合原语更新。 证明理论依赖于一个公理，通过应用程序的空事务，连同四个推理规则的事务定义应用程序，数据库查询，数据库原语更新和原子事务执行状态数据库不变性。3.3框架逻辑与事务逻辑的集成由于FL通过引入新的项扩展了FOHL，而STL和CTL通过引入新的连接词扩展了FOHL，所以这些扩展是正交的，可以直接组合，分别得到STFL 和 CTFL 。 准 确 地 说 ， 它 是 CTFL （ {insert （ Fact ） ， delete（Fact），send（Channel，Fact），receive（Channel，Fact）}），我们建议它作为UML ac的形式语言96F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-109活动和类图语义。虽然目前还没有CTFL的编译器，但执行平台可用于其两个子集：（1）Flora [32]，编译并高效执行STFL程序，（2）CTR6解释CTL程序。这两个平台都被实现为表格演绎引擎XSB [24]之上的层，XSB是Prolog的一个变体，依赖于称为SLG的另一种基于解析的FOHL定理证明过程。这个过程使得XSB比标准的Prolog更加声明性和高效。它实现了将否定作为失败的良好基础语义[29]，并缓存部分证明结果以避免低效的冗余计算和标准Prolog的左递归终止问题为了直观地总结CTFL形式主义和工具以及UML活动图和类图之间的关系，我们在图5中给出了我们方法的UML Meta模型[18]。4将UML类图和一组活动图映射到CTFL程序在本节中，我们将展示UML活动图和类图元素到CTFL构造的映射。 一个CTFL类定义事实base给出了类图的语义。CTFL规则库给出了活动图的语义。在下面的内容中，我们将每个主类图和活动图元素的通用模式与相应的CTFL构造模式相关联，CTFL构造模式在我们的建议中定义了它的形式语义。4.1将UML类图映射到CTFL类定义事实库(1) 类映射UML类签名直接映射到FL类定义项上，如图6所示。UML中具有布尔值的属性和方法在FL中不具有任何返回值。这是因为，每个FL属性或方法隐式地具有两个结果：它的逻辑真值（布尔值）和它的对象标识符。6 http://www.cs.toronto.edu/bonner/F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-10997图五、我们的UML AD和CD CTFL语义建议的元模型见图6。 类映射98F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-109(2) 关联作图UML关联被映射到关联类的FL属性上，遵循多重性约束。例如，在图7中，class1有一个引用classe2的集值属性，反之亦然。见图7。 关联作图(3) 专业化映射UML专门化关系被映射到FL子类UML属性和方法的默认可继承性被映射到类型约束操作符上，该操作符前缀为 *，它在FL中捕获了这样的语义。在3.1节中讨论了上述三个映射的RL案例研究见图8。 继承映射4.2将UML活动图映射到CTFL规则库活动图中的每条路径都映射到一个CTFL子句上，该子句的结论对应于图所建模的整体活动。然后，每个路径的节点和转换被映射到遵循以下规则的相应CTFL子句的前提上。F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-10999(1) 映射操作状态一个没有OCL约束的动作状态A被映射到CTFL项（即一个F-分子或一个以F-分子为自变量的谓词）上，CTFL项作为前提出现在表示A出现的活动图路径的每个子句中。图9中显示了这种通用映射。这是例如图2中的动作状态A8到图10中的规则1-3中的LA[cancelBurning（）]项上的情况。这样的映射也可以用于具有OCL约束的动作。然而，在这种情况下，增加了一个附加条款，其中的行动作为结论，八达通公司作为前提的限制7.见图9。 动作状态映射这是例如从图2中的动作状态A1到CC[checkCard（CC）]项的映射的情况，该映射作为图10中的规则6的结论和规则2-4中的前提出现。7将逻辑OCL表达式映射到CTFL前提超出了本文的范围100F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-109- -⊗ − ⊗ ⊗ ¬⊗← Ⓢ⊗−¬F. Ramalho等人/ Electronic Notes in Theoretical Computer Science 95（2004）83-10999• 规则1：路径A0、A8LA[burn（Pts，SI）]←（LA：loyaltyAccount）LA[membership[programs−>>LP：loyaltyProgram，customer−>>C1：customer]]<$LP[checkEnrolled（C1）]• 规则2：路径A0、A1、A8LA[burn（Pts，SI）]（LA：loyaltyAccountLA[membership[programs>>LP：loyaltyProgram，customer>>C1：customer，card>CC]]CC[所有者>C1]LP[checkEnrolled（C1）]CC[checkCard（CC）]LA[cancelBurning（）]）。• 规则3：路径A0、A1、A5、A8LA[burn（Pts，SI）]←（LA：loyaltyAccount）LA[membership[programs−>>LP：loyaltyProgram，customer−>>C1：customer，card−> CC]]CC[owner−>C1]SI：serviceItemLA[burnServiceItem（SI，LA）]burnLA [cancelBurning（）]）。• 规则4：路径A0、A1、A5、A6LA[burn（Pts，SI）]←（LA：loyaltyAccount）LA[membership[programs−>>LP：loyaltyProgram，customer−>>C1：customer，card−> CC]]CC[owner−>C1]SI：serviceItemLA[burnServiceItem（SI，LA）]LA[completeBurning（SI）]）。• 规则5：状态A0LP[checkEnrolled（C1）]← C1：客户登录LP[customer−>>C1]。• 规则6：行动状态A1CC[checkCard（CC）]← CC：customerCard验证 CC.valid.• 规则7：行动状态A6LA[completeBurning（SI）]← SI：serviceItem（插入（：burning[points→SI.points，status→completed]））。• 规则8：行动状态A8LA[cancelBurning（）] ←（insert（：burning[status→ canceled]））。图10个。CTFL规则库给出形式语义并实现图2的AD(2) 映射活动状态活动状态D被映射到一到四个CTFL项上，这些CTFL项在表示D出现的活动图路径的每个子句中图11中显示了这种通用映射。在最简单的情况下，活动既没有进入条件，也没有退出操作或中断事件，单个前提由包含方法D调用的CTFL项组成这是例如从图2中的A5活动状态到图10的规 则 3 中 的 LA[burnServiceItem （ SI ， LA ） ] 前 提 和 规 则 4 中 的LA[burnServiceItem（SI，LA）]前提的映射的情况。100F. Ramalho等/ Electronic Notes in Theoretical Computer Science 95（2004）83-109见图11。 活动状态映射在最复杂的情况下，所有可选元素都存在，每个元素都有一个额外的前提。三个前提按以下顺序被组合成一个连续的合取：进入动作，然后是复杂活动D，最后是退出动作。这个串行连接由一个原子模态操作符包围，如果在执行退出操作之前发生中断，则回滚进入操作和复杂活动D的副作用。这个事务在并发分离中与一个可能中断的事件连接。在所有情况下，整个活动图映射过程都被递归地重新应用到子活动图上，子活动图进一步指定了行为D。这导致在CTFL计划中引入新条款。 这 是例如图3的活动图到图12的规则的递归映射的情况。(3)映射fork和join对活动图中fork和join之间的并发节点直接映射到CFTL并发连接。这个并发合取是串行合取的中心元素，串行合取从引导到分叉的转换上的守卫开始，并以守卫在 连接后的过渡。图13中显示了这种通用映射。(4) 使用同步状态在UML活动图中，同步状态条可以在并发线程中用来表示同步状态。这些同步状态被映射到同步原语，在我们的正式语义建议参数化CTFL从另一个线程到这种同步状态的传入弧被映射到每个CTFL子句中的receive（Channel，done）前提，CTFL子句表示同步状态出现的活动图路径从这种同步状态到另一个线程的传出弧被映射到每个CTFL子句中的send（Channel，done）前提，CTFL子句表示同步状态出现的活动图路径Channel参数用于标识传入弧来自的其他线程或传出弧去往的其他线程。这些发送和接收动作是联合的