UML-RSDS: UML的精化模式和代码转换

理论计算机科学电子笔记137（2005）131-149www.elsevier.com/locate/entcsUML的精化模式K. 拉诺1号部计算机科学伦敦国王K. Androutsopolous2部计算机科学伦敦国王D. 克拉克3号部计算机科学伦敦国王摘要本文描述的策略或保留字：UML-RSDS，细化，模型转换1介绍UML是一种广泛使用的面向对象规范和设计的符号，它也是一个国际标准。与对象约束语言（OCL）一起，它代表了形式和图形规范的融合1电子邮件：kcl@dcs.kcl.ac.uk2电子邮件：kelly@dcs.kcl.ac.uk3电子邮件：david@dcs.kcl.ac.uk1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.04.028132K. Lano等人理论计算机科学电子笔记137（2005）131重组、模块化UML-RSDS规格一致性、完整性检查Java测试综合一致性B检查合成物业SMV检查合成B规格SMV规范Java代码这些语言有很大的潜力将正式规范技术的好处在本文中，一个子集UML-RSDS [10]将被用作UML中精确规范的语言，并说明如何定义将UML规范细化为可执行代码的系统规则。图1显示了UML-RSDS及其附带工具集支持的整个开发过程。开发人员可以使用该工具构建分析或设计类图和状态机，分析这些以符合UML或特定于平台的元模型（目前仅支持Java和基于Java的Web系统），转换模型以提高其质量或细化它们，转换为B [7]或SMV [1]进行语义分析，并从Java UML模型生成Java代码。还提供了一个用于从类图生成Web系统（在MVC架构中使用Servlet和JDBC）的专用工具。Fig. 1. UML-RSDS过程2UML中的规范UML规范可以由许多不同的互补模型组成，例如用例模型，类图，序列图等，我们在这里只考虑类图，状态图和约束图2显示了一个典型的Scrabble游戏系统的类图，由具有属性和操作、关联、继承和约束的类约束可以放置在许多UML元素上：• 类，作为类的不变量，给出与类的不同特征相关的属性。例如，W ord上的constraintendx =startx或endy=starty意味着单词对象必须是垂直的（第一种情况）或水平的（第二种情况）。• 操作，作为操作的前置和后置条件，定义操作的行为例如，setSymbol（c：char）上的约束pre：score= 0表示只有分数为零的空白字母可以用作任何字符。K. Lano等人理论计算机科学电子笔记137（2005）131133游戏板板placeMove（m：x：1..15平方% 1isOccupied（）：111移动）y：1.. 15boardSquaregetSquare（i：1.. 15,j：1. 15）：广场0..11getLetterScore（）：整数placeLetter（l：信）post：squareLetter = {}=> result = falsepost：squareLetter /= {}=> result = true1猎物袋11球员{ordered}二 ... 4球员name：String{identity}score：00.. 1{disjoint}袋0.. 100字母squareLetter0..1信100symbol：charrack字母得分：联系我们0..7setSymbol（c：111字典1PlayerRack0个..1机架/rackSize：0..7addLetters（l：Set）1 * wordLetters{ordered}* 查找（w：Word）电脑播放器历史{ordered}allWords联系我们*文本1{ordered}*评分：1000..1LetterMove- -词*x：1..151letterMovesy：1..150.. 1score：1000..15starty：1.. 15{ordered}*endx：1..15endy：1..15话getScore（b：成型机validateMove（n：n）：布尔calculateScore（b：Board）：整数移动HumanPlayer三字方块双字方块三字母广场双字母广场普通广场endx = startx或endy = starty字符串前：评分= 0post：squareLetter = l游戏turn：1.. 4个动作编号：整数startGame（）gameEnded（）：布尔袋/bagSize：0..100isEmpty（）：Boolean giveLetters（x：）：Set*图二. Scrabble类图• 关联，给出描述关联末端的类中哪些对象对可以通过关联连接的约束wordsFormed.text<：allWords在游戏移动和游戏字典的关联上表示，在拼字游戏的接受移动中形成的所有单词必须在字典中。2.1UML-RSDS约束LOCA（对象、约束和关联逻辑）语言[10]或OCL（http：//www.omg.org/ocl）可以用来定义约束，UML-RSDS模型。然而，UML-RSDS在标准UML类图上的重要扩展是约束可以附加到关联：附加到关联集合的约束将由这些关联链接的所有对象对的集合作为其上下文。这意味着在许多公式中，量化器或对特定对象的引用可以完全避免134K. Lano等人理论计算机科学电子笔记137（2005）131C1OnOff状态枚举>>例如，约束C1：aatt=On→batt=On图3中的a：A;b：B·（a，b）∈AB其中A B是A和B之间的关联程度。一brBaatt：状态batt：状态- -图三. 简单类图与OCL导航表达式相比，关联约束允许更抽象和更少的实现偏差的属性规范：OCL导航表达式总是从特定类的上下文开始表达属性，因此将规范偏向于该类负责维护约束的实现。与OCL中使用的导航表达式相比，关联约束对模型结构的变化更具弹性：公式通常可以保持不变，只有它所链接的关联集需要改变。LOCA是OCL的一个简化子集，旨在更容易教授和使用，避免使用量化器等数学结构，并简化OCL语法。LOCA中省略了OCL的元模型特性：oclIsTypeOf、oclIsKindOf、oclIsN ew、oclAsT type、allocation、OclT type、oclInState、OclState、OclAny、OclExpression。在 LOCA 中 ， x.oclIsKindOf （ t ） 可 以 表 示 为 x ： t ， 用 于 类 名 t 。x.oclInState（s）可由x.att=s表示，其中s是附加到类的状态机的状态，att是标识当前状态的属性。C. allanc（）由名称C本身表示。LOCA中也省略了OCL的程序操作符， 是袋子和有序的集合类型。表1显示了在UML-RSDS工具中，UML-RSDS约束中当前接受的LOCA表达式的语法。valueseq是一个逗号分隔的值序列。因子级运算符op1可以是：K. Lano等人理论计算机科学电子笔记137（2005）131135<值>：：=<身份识别> |number<>||<产品介绍：：=<身份识别>|. <身份识别>|< 产品介绍|（<表情>）：：=<产品介绍|[ value>]<因数>：：=<值>|联系<我们|序列{}| arrayref<>|<因子>op1<因子><表达式1>：：=<因子>op2<因子>：：=<表达式1>|（<表情>）|<表达式1> op3<表达式><静态不变>：：=|<表达式>=>表达式><时间不变>：：=+|=> temporalop>+ expression>表1失水事故（i）+、−、、/、div、mod(ii)\/，/\（也写作和），↑比较器运算符op2是=、/=、、>、=、>=、：、：、/：、/<：中的一个。逻辑运算符op3是或之一。 时间算子是AX（在所有下一状态中）、EX（在某个下一状态中）、AF（在所有路径上的某个未来状态中）、EF（在某个路径上的某个未来状态中）、AG（在所有路径上的所有未来状态中）和EG（在某个路径上的所有未来状态中）中的一个。标识符是类名、函数名、类特征（属性、操作或角色名）、枚举类型的元素，或者表示变量或常量（如果是大写）。变量在整个公式中被隐含地普遍量化。操作也可以用参数写为op（p1，.，pn）等。UML-RSDS工具目前支持的函数有：size，toU per，toLower用于字符串和大小，asSet、max、min、sum、prd用于集合（集合和序列），rev、sort用于序列，sqrt、sqr、floor、round、abs用于数字。136K. Lano等人理论计算机科学电子笔记137（2005）131计划扩展八达通卡的其他功能2.2操作约束UML-RSDS开发的推荐方法是仅使用声明性约束来指定系统：不引用操作的约束，K. Lano等人理论计算机科学电子笔记137（2005）131137名字。声明性约束定义了系统的不变属性，而不偏向于维护它们的特定算法，因此它们在MDA术语中形成了计算独立模型（CIM）。如本节所述，从这些模型中可以系统地推导出更明确的业务模型。一个声明性的UML-RSDS规范包括一个UML类图，定义类图中类的预期生命历史的协议状态机，以及类图中类和关联的声明性约束。声明性约束，如图3中的aatt=On→batt=On，可以解释为描述系统必须执行的响应使约束的前提为真的事件。在这种情况下，如果在某个A对象ax上发生事件setaatt（val），将ax.aatt设置为val，并且val=On，则约束（C1）将要求在与ax相关的所有B对象上执行setbatt（On）。因此，约束的操作形式为setaatt（val）val=On→AX（batt=On）其中AX（P）断言P在“下一个”状态中成立，即在对事件的反应终止时的状态。这与OCL后置条件约束的含义相同。一般来说，根据关联rs上的声明性约束I：PG→Q我们可以推导出，对于每一个可能影响I的真实性的事件α：αP1→AX（G[e/v] →Q[e/v]）其中v是I的自由变量，对于某个表达式e，当P1为真时（假设α不修改任何rs），α在其终止处建立P[e/v]αP1→AX（P[e/v]）E[e/v]表示用表达式e替换E中的标识符v。对 于 每 一 个 事 件 α ， 其 形 式 为 特 征 f 的 setf ， 或 多 值 角 色 r 的 addr ，remove，UML-RSDS工具确定由α约束的约束集，即，那些其前件可以由α变为真的约束。这些被收集在一起，从它们导出的更新被用来定义系统对α的响应：这个响应是为了保持被检验的不变量的真实性所需要的。该算法是Java和B综合过程的基础，也可用于生成其他语言的代码，如C++或C#。138K. Lano等人理论计算机科学电子笔记137（2005）131例如，如果类不变式具有以下形式：att=vatt 1 = v →att2 =v 2对于类的属性att、att1和att2，则setatt是：setatt（x）x=v→AX（att1 =v 1 →att2 =v 2）AX内部的含义用于合成setatt操作的代码，例如：public void setatt（T x）intx;如果（x==v）{if（att1== v1）{setatt2（v2）;}}}3UML模型UML模型可以被系统地转换，以将它们细化为更接近于在特定平台上实现的例如，消除关联类（在任何主流OO编程语言中都无法表达），消除多对多关联（用于关系数据模型的细化）等。一个有用的细化变换，它降低了程序中数据的复杂性，是：名称将关联变为索引这将用整数索引替换标识角色集成员的关联i动机由此产生的数据结构更简单，更容易实现。条件的关系br.size>0→i =br[index]在原始模型和改进模型之间。精化转换的另一个例子是引入for-eign键来表示两个持久化实体之间的显式多-一关联名称用外键替换关联K. Lano等人理论计算机科学电子笔记137（2005）131139Bi*一br.size > 0 =>i：br0.. 111br {已订购}见图4。 将索引关联转换为属性这种转换适用于持久类之间的任何显式多对一关联。它假定关联所链接的类的主键已经存在。它通过将关联的“一”端的实体的键的值嵌入到“多”端的实体中来替换关联这是在关系数据库中实现数据模型的基本步骤。特别是，它可以用于在这样的数据库中实现Web应用程序这在图5中显示。一akey：T{identity}1*Bbkey：S{identity}图五. 用外键替换关联条件b.akey等于a.akey，当a›→b在原始关联中时：（a，b）∈A Bb.akey=a.akey必须通过实现addbr和removebr操作中的外键值。为了应用这种转换，UML-RSDS工具的用户从当前模型中的多对一关联列表中选择多对一关联，然后在一个新的模型中创建一个新的多对一关联。1*br {已订购}网站首页&index = br.sizeB公司简介一akey：T{identity}一bkey：S{identity}akey：TB140K. Lano等人理论计算机科学电子笔记137（2005）131生成带有外键的模型，替换原始模型。新属性被标记（定型）为外键，以便在生成的Web系统中生成正确的SQL，用于查找和修改关联[12]。在操作的前/后指定上的通常精化演算变换是有效的[13]：名称弱化前置条件或强化后置条件描述一个操作的前提条件可以被削弱（因此该操作可以应用于更多的情况）和/或其后置条件可以被加强。=> Q1 }见图6。 弱化前置条件/强化后置条件4约束实现通过考虑模型的约束，可以进行更多的细粒度细化变换。以下定义将用于定义细化可执行代码约束的策略。定义：写入帧wr（Code）表示可由Code修改的对象特征集。例如，obj.setf（x）有写帧{obj.f}，E.setAllf（objs，x）有写帧obj.f的集合，其中obj∈objs。写入帧还考虑了更新的间接影响。 如果存在同一类的另一个特征g，其（对于每个对象）取决于f的值，则这些写入帧是{obj.f，obj.g}和{obj：奥布日斯|奥比约f} {o bj：o bjs|奥比约g}。定义：自由（E）对于表达式E，free（E）表示E中引用的对象特征的集合。因此free（obj.f= 1+obj.g）是{obj.f，obj.g}。一{ P1 => P2，运算符一运算符发布时间：Q2上一页：P2发布时间：Q1上一篇：P1K. Lano等人理论计算机科学电子笔记137（2005）131141定义：查询表每个LOCA表达式e在Java中都有一个解释eJ，这是基于特定上下文中每个对象集上的变量。对于实体E，设vare是在E的对象集合上变化的变量。然后我们有表2中给出的解释。LOCAJava变量、常量、字符串或原始值x实体E的属性att实体E的作用obj.f其中obj是单个对象objs.f其中objs是一组E类型的对象。x：yx /：yx=y对于基元x，y x=y对于对象x，y x div yx modyxyx-y对于集合x，y{x1，.，xn}xyPQP或Qe[i]Xvare.getatt（）vare.getrole（）objJ.getf（）E.getAllf（objsJ）yJ.contains（xJ）！（yJ.包含（xJ））xJ==yJxJ.等于（yJ）xJ/yJxJ%yJSystemT types.Set.union（xJ，yJ）SystemTypes.Set.subtract（xJ，yJ）（new SystemT ypes.Set（））.add（xJ）.1... .add（xJ）.getElements（）nSystemT types.Set.intersection（xJ，yJ）PJQJPJ||QJeJ.get（iJ−1）表2LOCA表达式的Java查询形式142K. Lano等人理论计算机科学电子笔记137（2005）131定义：更新表给定某些形式的后置条件/约束结论X，可以定义一段相应的程序代码CodeX，它确保X在CodeX执行后保持：[CodeX]X。表3显示了基本情况。在表中，仅存在更新表单LOCAJavax：目标作用角色集值，单对象obj。E的多个对象if（obj.getrole（）.contains（xJ））{}intn=nums（nums）;E.addAllrole（objJ，xJ）;x /：obj.rolerole多值objJ.removerole（xJ）;obj单值E.removeAllrole（objJ，xJ）;obj集值，类型FIN（E）目标f=xobjJ.setf（xJ）;obj单值E.setAllf（objJ，xJ）;obj集值，类型FIN（E）结果=valreturnvalJ;val：结果return.add（val）;表3LOCA表达式如果要更新的特性是可修改的，即它不是只读特性 在UML模型中（在UML-RSDS中，我们也禁止更新表示传感器或其他输入数据的输入属性）。如果约束的后继项没有更新表单，则后继项的查询表单将添加到实现该约束的每个操作的前提条件中。在拼字游戏中，wordsFormed.text<：allWords就是这种情况，所以addwordsF ormed（wd）具有前提条件wd.text：allWords.K. Lano等人理论计算机科学电子笔记137（2005）1311431n4.1连词修饰给定一组类或关联不变量，可以生成用于操作setf、addr、remove的代码，用于由不变量链接的类/类的任何特征f或角色r。 此代码旨在通过修改功能来响应操作，或者通过断言先决条件来防止在违反不变量的情况下调用操作，从而保留不变量。这种代码合成过程通常可以以组合的方式进行，即，用于不变量的不同子集S1和S2的代码可以是syn-sign的。论文分开，然后结合起来，以提供代码的S1和S2。一对约束A→B C→D可以实现如果（如果（但条件是：wr（代码B）wr（代码D）=wr（代码D）无干扰（AJ）=无干扰第一个条件是必要的，因为否则代码D可以撤消代码B实现的更改。第二个是必要的，这样代码D就不能使AJ为真。这一规则的一般情况是：A1→B1.An →Bn可以实现如果（AJ）{代码B1}.如果（AJ）{代码Bn}但条件是：wr（代码Bi）wr（代码Bj）=for i/=jwr（代码B）free（AJ）=forj

下载后可阅读完整内容，剩余1页未读，立即下载