沙特国王大学学报：基于模式的模型重构与引种关联关系的案例研究

Journalof King Saud University沙特国王大学沙特国王大学学报www.ksu.edu.sawww.sciencedirect.com基于模式的模型重构引种关联关系Boulbaba Ben Ammar*，Mohamed Tahar Bhiri突尼斯斯法克斯大学斯法克斯科学学院接收日期：2013年10月9日;修订日期：2014年3月12日;接受日期：2014年6月5日2015年4月16日在线发布摘要重构是一个重要的软件开发过程，涉及到模型的重构，以提高其内部质量，而不改变其外部行为。本文提出了一种基于UML、B和CSP相结合的模型重构方法。UML模型由类图、OCL约束和状态机图描述。我们详细介绍了一种重构模式，它允许在两个现有类之间引入关联关系。我们说明我们的建议，给出一个案例研究涉及SAAT（软件架构分析工具）系统。2015作者。制作和主办：Elsevier B.V.代表沙特国王大学 这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。1. 介绍重构是一种重组活动，旨在改善现有代码体的内部结构，同时保持其外部行为。此活动增强了软件系统的质量特性，包括可扩展性（在演化维护期间）、可重用性和效率。在代码重构技术的文献中已经提出了各种方法。例如，Fowler（1999）提供了一个适用于Java程序静态部分的重构规则目录，包括*通讯作者。电 子 邮 件 地 址 ： Boulbaba. live.fr （ B.Ben Ammar ） ，Tahar_Bhiri@yahoo.fr（M.T. Bhiri）。沙特国王大学负责同行审查“ExtractClass” 、 “MoveOperation” 、 “MoveAttribute” 和“RenameOperation”。最近，重构技术也被几种敏捷软件开发方法所采用（Shore和Warden，2007），如XP（Baumeister和Weber，2013）和Scrum（Schwaber和Sutherland，2013）。事实上，它们涉及测试驱动开发（TDD），这是一个快速的周期，包括三个阶段：测试，编码和重构。重构工具也可用于大多数面向对象语言，包括Java、Smalltalk、C++、C#、Delphi和Eiffel，以及用于集成开发环境，如Eclipse、NetBeans和Oracle JDeveloper。然而，这些代码重构规则经常被非正式地定义，模型质量和规则之间没有建立任何关系。最近已经进行了几次尝试来克服这种不足，特别关注重构技术在标准模型上的应用，包括UML（Mens et al.， 2007年）。在本文中，我们提供了一种新的方法，模型重构的基础上结合使用UML，B（Abrial，1996），http://dx.doi.org/10.1016/j.jksuci.2014.06.0121319-1578年，作者。制作和主办由爱思唯尔B.V.代表沙特国王大学。这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。制作和主办：Elsevier关键词模型重构; UML;B级;CSP;关联关系引入关联关系的基于模式的模型重构171和CSP（Hoare，2004）。UML模型由类图、OCL约束和状态机图描述。具体来说，我们提出了一个重构模式的目录，这些模式在同一个框架中描述，并形式化为B和CSP。这些重构模式涵盖了面向对象方法的基本概念：类之间的概念关系（关联和泛化/特化），多态性，重新定义，抽象类和泛型类，以及委托。应用重构后的行为保留被分配给与B（Atelier B的证明器 （ Engineering ， 2009 ） ） 和 CSP （ 模 型 检 查 器 FDR2（Goldsmith，2005））相关的工具。事实上，一些研究人员已经定义了将UML翻译成B的系统规则（Idani等人，2009年）和CSP（Rasch和Wehrheim，2003年）语言。之前有几项研究报告了B方法在开发各种复杂的现实应用中的成功应用，包括巴黎市的第一个无人驾驶地铁METEOR项目（Behm等人，1999年）。这种方法代表了少数几种正式的方法之一，这些方法在整个开发生命周期中具有强大的商业支持工具，从规范到代码生成。虽然强烈建议使用此方法来验证静态属性（如安全性），但它不用于检查动态属性（如活性）。出于这个原因，我们选择使用CSP语言。本文其余部分的结构如下。第2节将概述与正在调查的专题有关的工作。第3节将定义我们提出的方法。在第4节中，我们将给出重构模式的一般在第五节中，我们将详细介绍关联关系的引入模式.第6节将通过使用SAAT系统来说明我们的建议。最后，总结了本文的主要研究成果，并对模型重构研究提出了新的展望。2. 相关作品表1总结了到目前为止为UML模型使用文献中通常引用的一组评价标准。根据MDE方法，重构可以被认为是一个事务处理系统（Mens和Gorp，2005），它引入了对模型结构的更改（不添加与被认为是垂直模型转换的精化不同，重构是水平模型转换。换句话说，重构过程不会导致抽象级别的变化：源模型（重构之前）和目标模型（重构之后）仍然处于同一个抽象级别。在软件驱动的工程模型中，重构技术非常有限（Allemand Mens，2007）。一些研究人员（Gorp等人，2003，Mens，2006，Mens等人，2007年，Mens和Tourwe，2004年）表明，考虑整个模型重构过程仍然是一项具有挑战性的任务。这一进程包括六项主要活动：1. 确定模型的哪些部分应该重构。2. 决定哪些重构规则应用于哪些区域。3. 确保一旦应用重构，将保持模型行为和一致性。4. 使重构的应用程序5. 评估重构对软件质量标准（复杂性、易读性、适应性）或过程（生产率、成本、工作量）的影响。6. 重构模型和其他工件，如源代码，文档，规格和测试。Markovic（2008）中描述的工作提供了一个重构操作的目录，其灵感来自于Fowler（1999）描述的预重构操作列表。所提出的操作适用于类图，并表示基于QVT的形式化模型转换。重构操作对OCL约束和对象图的影响也已经被描述。其他研究人员（Gorp等人，2003）提出了UML元模型的扩展，允许在重构中更好地指定两个前/后操作符：“PullUp Method”和“Extract Method”。此扩展还赋予了其他功能的工具：检查前置/后置条件，表1 UML模型重构方法的相关工作总结方法03 The Dog（2008）Men（2006）vanMens等人马尔科维奇苏尼河科雷亚男人和Kempen（二零零七年） 关于Baar等人和05 The Dog（2005）等人（2005年）（二零零八年） （2001年）Werner（二零零七年）考虑阶级是的部分没有是的是的是的没有图审议国家没有没有是的是的没有是的没有机图八达通卡的考虑是的是的没有没有是的没有是的约束行为保全转变元建模UML到UML到图图重写重写模型形式化CSP语法进入QVT过程工具支持QVTOCL查询引擎支持Fujaba for the形式主义没有没有CSP图基于图转型语法检测没有设计味道没有最适合没有没有OCL重构重构闻起来172B.本·阿马尔，麻省理工学院布里编写重构操作序列，并使用OCL查询引擎检测“设计气味”（设计气味）。实际上，总体思路是提供原子转换或重构的基本规则。它们可以被视为重写规则，可以为一致的重组提供基础。因此，重构活动引起的潜在错误发生率将大大降低。Markovic和Baar（2008）还提出了一套重构规则，适用于考虑OCL约束的基本类图。他们的规则受到了以前在重构面向对象语言中提出的规则的启发（Mens和Tourwe，2004）。作者将重构模型定义为一组转换规则，由七个重构规则组成，它们对附在重构类图上的OCL约束的语法有或没有影响。作者还使用图语法形式主义来检查行为保持。在Sunye'etal. （ 2001）有两个重构规则列表。第一个列表适用于类图，有五个基本操作：这里值得注意的是，元素可以是类、属性、操作或关联端。第二个规则列表适用于状态图表，包含七个基本操作：“这些操作的语义在OCL中定义。在另一项研究（Correa和Werner，2007）中，重构技术被用于改善对OCL规范的理解和维护。作者确定了OCL使用不佳的实例（OCL气味），并提供了足够的重构操作集合以防止其发生。在作者确定的OCL气味中（十几种），我们可以引用：Reimann etal.（2010，2012）提出了一种基于角色模型的新方法来指定泛型重构，从而解决了以前工作的局限性，并将特定重构定义为泛型重构的扩展。该方法基于Eclipse建模框架（EMF）实现，并使用多种建模语言和重构进行评估。在Einarsson和Neukirchen（2012）中，作者提出了自动化重构，这些重构是为了使用QVT操作转换语言重构UML活动模型及其图形表示，以转换使用Papyrus UML编辑器创建的UML模型和上面提到的方法没有同时处理由类图、状态机图和OCL约束描述的UML模型。这个限制并不能帮助我们在重构之后验证两个基本属性的保留，即安全性（类图和OCL约束）和活跃性（状态机图）。模型重构的另一个问题是行为保持。根据定义，模型重构应该保留它所转换的模型的可解释行为。为了实现这一目标，我们建议将模型转换为正式语言，如B和CSP。2.1. UML基本概念UML定义了类之间的四种关系关联关系：它描述了类之间的一组链接或连接。 在面向对象语言中，这种概念关系被称为客户关系。特殊化/泛化关系：这是一种概念关系，允许一个类（称为子类）继承其父类（称为超类）的特征。在面向对象语言中，特殊化/泛化关系被称为继承关系。实现关系（Realization relationship）：它是一种接口定义由实现类保证的契约的关系。依赖关系：它不一定需要类之间的链接，并表明一个元素或一组元素需要其他模型元素来指定或实现。依赖关系由从依赖者（或客户端）指向 供应商（Supplier）事实上，UML定义了其他几个概念。我们在下面描述一些与我们的工作有关的概念委托：一个类可以将它的部分活动委托给另一个类。在UML中，操作委托机制由连接两个类的组合或聚合关系来领导。泛型类：类可以有表示类型或变量的正式泛型参数。在UML中，泛型类被称为类“模板”。我们不能直接使用模板，我们首先需要实例化器。实例化意味着通过依赖“bind”将模板的那些形式泛型参数绑定到真正的泛型参数，这给出了一个可以像任何普通类一样使用的具体类。与Eiffel（Meyer，2000）等其他编程语言相反，UML不支持需要引入遗产的强制泛型：表示类型的正式泛型参数必须从升序类型向下。多态性：在面向对象的开发过程中，变量实体或数据结构的元素可以采取几种形式，在执行期间，在静态声明的控制下与不同类型的对象连接。2.2. B方法受Dijkstra （1975 ）和Hoare （2004 ）的启发，B方法在Jean-Raymond Abrial的B Book（Abrial，1996）中得到了阐述和正式定义。它涵盖了软件开发的所有阶段，从规范到实现，通过精化的概念，允许严格表达规范所需的属性。B方法的目的是产生一个安全和准确的软件结构。事实上，B语言被认为是Z语言的演变，旨在为整个开发周期以及实际的工业应用开发一种合适的方法。B方法区分两种类型的证明：不变量的守恒和精化的正确性。不变量一致性检验模型一致性和不变量性质的证明，引入关联关系的基于模式的模型重构173>Ps< $ut2CPt;其中s是简单状态，CsM1/1我的天啊！其中s是一个简单的状态，而C s;;其必须在操作的初始化时和执行操作之前/之后被保存。精化正确性的证明确保了具体模型与抽象模型的一致性。这些证明义务是使用与B方法相关的工具自动生成的。2.3. CSP语言概述CSP过程是根据与对象描述相关的事件来定义的所有这些事件的名称都被称为字母表。进程最简单的行为是什么都不做，这个进程用STOP表示。为了描述更复杂的行为，CSP提供了一些操作符，如：前缀、递归操作符、确定性和非确定性选择、隐藏事件、并行组合、输入/输出、交织和量化。CPS的三个语义域（Roscoe，1994）是稳定痕迹、失败和失败-分歧。流程行为的稳定跟踪是指该流程在给定时刻参与的有限事件序列。一个过程P的所有可能的迹的全集用迹（P）表示。然后，模型考虑与每个过程P相关的稳定故障，其中涉及对（t，E），其中t是指P和E接受的有限组迹，这些迹是过程在运行t的事件后不能运行的事件集。所有这些对都表示为失效（P）。CSP模型8>Ps¼SKIP;其中s是最终状态;S2.5. 将UML的行为方面转换为CSP在本节中，我们描述了Rasch和Wehrheim（2003）提出的将状态机图转换表2给出了本文其余部分中使用的名称分配约定。UML的翻译功能！状态s的CSP在CSP中定义>>：Ps¼jjjnPÞ;ððut其中s是子状态机M i;还允许描述P的死锁。事实上，如果E等于P的可执行事件的集合，则P被阻塞。最后，该模型考虑了与每个过程P相关联的失败-分歧集，其中涉及其所有潜在失败和分歧的集合。一个过程P是在一个发散状态，只有当它是在一个状态，其中唯一可能的事件是内部的。P的发散集记为发散（P），它是迹t的集合，使得进程在运行t之后发现自己处 于 发 散 状 态 。 如 果 过 程 是 确 定 性 的 ， 那 么divergences（P）是空的。2.4. 将UML的结构方面翻译成B语言已经提出了几种将UML图转换为B的方法（Idani等人，2009年）。一些研究（Ledang，2001; Meyer and Souquie`res，1999）建议开发一种同时考虑多个UML图的详尽方法。其他工作（Laleau，2002年）侧重于数据库领域，安全的SQL代码然而，其他研究（Lano等人， 2004;Snookand Butler，2004）提出了一个B profile来使用UML。转换函数uUM L！子机的CSP在CSP中定义如下：uUML！CSPM在计算uUM L！CSP将为任何s和uUM L！对于SM的任何子机M，对应于状态机图SM的CSP进程可以通过结合两个 获得的函数来 计算。CSP以及如下评估状态机M_top：PROCSM ¼ M顶部3. 该方法我们的方法包括在一个目录的重构模式，允许重组的UML/OCL类图的内部结构的发展。这些模式也可以转换状态机图，同时考虑引入类图的修改。这样的模式可以与重构规则相比较。建议的重构模式支持软件质量的改进，包括可扩展性、可重用性和效率，并允许模型设计者引入表2名称分配约定。SMsCsTsMMtopIM嗯！CSP跳停状态机图简单或合成状态% s的所有夫妇的集合，继承人的集合，通过由e高级状态机SM的一个子机M的初态集JJJ;将状态机图转换为CSP流程CSP流程僵局平行作文连续的作品Mi2Cs174B.本·阿马尔，麻省理工学院布里ðÞ继承关系、多态性、抽象类和泛型类、重新定义、关联和删除等概念。这些模式的特点是由四个步骤组成的精确框架：参数的识别，适用性的验证，规范的演变和模式的正确性。这些步骤展示了重构模式的基本方面。此外，所提出的重构模式在B中形式化，使用系统规则将类图及其OCL约束转换为B（Ledang，2001; Marcano和Levy，2002;Meyer和Souquie`res，199 9）和翻译函数uUML！CSP将状态机图转换为CSP过程（Rasch和Wehrheim，2003）。这有助于我们精确地识别应用程序的不同条件、UML类图的演化、OCL约束和状态机图以及模式的正确性。各种检查由AtelierB负责B规范，FDR2负责CSP工艺。这些建议可以作为重构模式最终自动化的里程碑。我们工作的主要思想是提出一个重构模式的目录，允许添加上面描述的各种关系和概念，目的是提高现有UML规范的质量因素。某些模式增强了非依赖类之间的新关系的添加，这表示需要将概念引入给定的类。与继承、关联、重新定义和多态相关的重构模式通过以下方式参数化：这两个相关的类，OCL约束附加到每个类，与每个类实例的动态属性相对应的状态机图。虽然重构模式与Ben Ammar等人（2008）的委托相关联，但泛型和抽象类由以下内容设置：● 相关类，● 附加到相关类的OCL约束，● 对应于相关类的状态机图4. 重构模式重构模式的应用包括四个步骤。我们首先确定它的参数。然后，我们确保这些参数满足一组条件。之后，我们将展示所选模式提供的不同更新。最后，我们检查产生的结果。因此，重构模式的定义由四个步骤组成，可以总结如下：1. 参数识别2. 适用性验证3. 规格演变4. 模式正确性4.1. 参数识别它以一个或两个包含相关类OCL的三元组的形式提供模式参数附加到相关类的约束，以及与相关类关联的状态机图：Class、OCL_Class、STD_Class。使用：类表示所涉及的类。它由一组静态属性（称为l attrClass）和一组动态属性（称为l meth Class）表征。OCL类表示OCL约束。这些约束附在Class上，由以下元素组成– I类：类的不变量，在每个稳定时刻必须检查类的所有对象的条件，1在OCL中形式化为：上下文类别invI类：条件– 对于l个meth类的每个方法meth类：*P meth Class ：操作meth Class的前提条件，在执行meth Class之前必须检查的条件，*Q meth Class ：操作meth Class的后置条件，在执行meth Class后必须检查的条件，在OCL中通过以下方式形式化Context Class：：meth Classpre P meth Class：conditionpostQmethClass：conditionSTD_Class构成状态机图，对类实例的行为建模。4.2. 适用性验证重构模式与识别的参数一起应用。建议确保这些参数满足以下两个条件：1. 模式的各种参数之间的一致性，这些参数分别涉及：类和OCL_Class之间的关系，方法是检查类的属性的OCL约束是否充分。类和STD_Class之间的区别在于可以根据STD _Class顺序执行调用的方法。2. 模式引入的概念的一致性（继承、关联、委托等）。列举的条件可以分为两种类型：● 那些与静态特性有关的，● 与动态特性有关的。为了检查与静态属性（安全属性）相关的条件，我们使用以下系统转换规则将类及其属性和OCL约束转换为B规范：从UML到B，如Ledang（2001年）和Meyer和Souquie`res（1999年）所提出的，从 OCL 到 B ， 如 Ledang 和 Souquie` res （ 2002 ） 以 及Marcano和Levy（2002）所建议的。1.“稳定时刻”对应于类的方法执行之后的时刻。在方法的执行过程中，类的不变式可能会被暂时违反。●●●●●●●●●●引入关联关系的基于模式的模型重构175IClass^PmethiClass）½QmethiClass]PmethjClassIClass^PmethiClass）½QmethiClass]P methkClass一可以在执行methi Class之后调用methj Class和methK Class与B相关的工具是Atelier B（Engineering，2009）。为了检查与动态属性（活性属性）相关的条件，我们使用函数uUML！CSP由Rasch和Wehrheim（2003）提出。检查CSP过程的工具是FDR2（Goldsmith，2005）。翻译成B和CSP的资源是因为没有直接检查UML/OCL规范的工具。在这方面，在文献中有几个建议涉及到将UML/OCL规范翻译成正式语言，并允许使用相关的工具。验证参数一致性的过程如下：将Class翻译成B机器，称为B_Class，将OCL_Class翻译成相应机器中的不变表达式，添加控制注释，由Ifill提出（Ifill等人， 2007年），在B机器的ASSERTIONS条款中。对于每个方法methiClass，断言包含以下形式的两个证明义务：所得到的B机的一致性证明了类与其约束OCL类之间的一致性.断言的验证证明了类与其状态机图STD类之间的一致性。随着分析的展开，将对每个模式描述模式引入的概念的一致性的验证过程4.3. 规格演变它展示了为UML/OCL规范自动实现的各种更新。4.4. 模式正确性它涉及：1. 保护重组班级的财产。2. 保留重组班级的行为。下面我们只描述重构模式的定义：引入关联的概念5. 模式的定义关联关系是两个或多个类之间的语义连接。它可以是二进制或n进制。协会的特点如下：其多重性用于指定两个或多个类之间的关系中每个类的实例的最小和最大数目，它的可导航性显示了如何从一个类访问到另一个类。如果关系在Class1和Class2之间，并且只有Class2是可导航的，那么您可以从Class 1访问Class2，但不能反向访问。这意味着虽然导航性在默认情况下是双向的，但关联是单向的。在UML中，一个类可以使用一个或多个其他类的一个或多个静态（属性）和动态（方法）属性。相应地，类必须与所咨询的类具有关联关系，具有对那些类的可导航性。在本节中，我们只介绍在涉及调用一个或多个方法时的二元单向关联。5.1. 参数识别引入关联概念的重构模式通过以下方式参数化：h 1类;OCL 1类;STD 1 i类h 2类;OCL 2类;STD 2 i类假设：类之间的关联表示方法调用，即，如果类1与类3有关联，那么类1至少调用类3的一个方法（见图10）。2）的情况。图1重构前的参数图2重构前的参数●●●●●176B.本·阿马尔，麻省理工学院布里ððÞÞððÞÞððÞÞððÞÞððÞÞððÞÞvððÞÞ5.2. 适用性验证为了使我们的模式具体化，我们假设，第二类的教育部分由第一类完成。因此，我们假设Class2以如下方式将其工作委托给连接的类：Class3执行操作3，然后Class4执行操作4，最后Class5执行操作5。类似地，Class1以如下方式将其工作委托给连接的类：Class3执行操作3，然后Class4执行操作4。类实例的行为由状态机图建模，被调用方法的检测由CSP进程验证。Class1和Class2的行为分别由进程PSM_Class1和PSM_Class2定义。PSMClass1 ¼ Class 3！三号行动！3级r？x的！四班！四号行动！4级r？x的！停止PSMClass2 ¼ Class 3！三号行动！3级r？x的！四班！四号行动！4级r？X！五班！5号行动！5级r？x的！SKIP因此，为了检查方法调用的存在，我们必须找到所描述的CSP进程的文本替换。5.3. 规格演变规范的演变包括：在Class1和Class2之间引入关联，具有从Class2到Class1的可导航性。抑制类2和类3之间以及类2和类4之间的关联。图 3表示重构后的规范状态。5.4. 模式正确性应用所提出的重构模式所做的更改保留了这两个类的属性，特别是Class1和Class2的静态和动态方面没有更改 。 事 实 上 ， Class2 和 Class3 之 间 的 直 接 关 系 被Class2 和 Class1 之 间 的 两 种 关 系 所 取 代 ， 然 后 是Class1和Class3。关联的链式分解的B规范的验证在BenAmmar（2012）中描述。状态机图STD_Class1和STD_Class2要求验证这两个图相对于其相应抽象级别的相似性是否被保留。因此，它足以表明：assertPSM Class1与PSM Class 1的比较assertPSM Class2与PSM Class 2的比较其中s指的是基于迹线模型的CSP细化。6. 为例为了说明我们的建议，我们采用SAAT（软件结构分析工具）系统（van Kempenet al.，2005年，作为例子。SAAT是一种分析工具，用于计算UML模型中的参数，然后可以用于分析潜在的模型或反模式的缺陷类：对应于SAAT系统的类图（见图4以下类：Saat;DB;Stat;DBCreate;Parser;DBFill;DBCheck;Analyse;StatCalc和StatFilter。这些类之间的关联表示方法的调用，即如果类A与类B有关联，则类A调用类B的方法。图4给出了对应于SAAT系统的初始类图。 Saat类以顺序 的 方 式 将 其 工 作 委 托 给 相 关 的 类 ： 数 据 库 被 创 建DBCreate：create，输入文件被分析Parser：parse，数据被插入数据库DBFill：fill。在插入数据之后，检查填充的数据库DBCheck：check。之后，数据将被分析Analyse：analyze，并计算统计数据StatCalc：计算并过滤StatFilter：根据用户定义的标准进行过滤。OCL约束：各种类没有重要的OCL图3重构后的参数图4重构前的类图●●引入关联关系的基于模式的模型重构177（a）DBCreate（b）Parser(c)DBFill（d）DBCheck(e)分析（f）StatCalc图7重构前的DB状态机图（g）StatFilter图5 DBCreate、Parser、DBFill、DBCheck、Analyse、StatCalcStatFilter的状态机图。图6 Statistics的状态机图状态机图：对应于各种类实例的行为在图1和图2中给出。 五比八图1和图2中所示的图表。图4-8显示了一种可以应用重构模式的情况：引入Saat和DB之间的关联关系。6.1. 参数识别图案的参数是：hSaat;OCL Saat;STD Saat ihDB;OCL DB;STD DB i6.2. 适用性验证在下文中，我们描述对应于来自SAAT系统的所有类从这些CSP进程中，我们推断PSM_Saat进程需要执行进程PSM_DB的方法调用序列。因此，这两个类之间的关联关系被证明是必要的。6.3. 规格演变重构模式在图4所示的类图上的应用生成了图4所示的类图。9.第九条。在这项工作中提出的重构模式被注意到，以改善SAAT应用程序的体系结构。事实上，类图在重构后显示的链接（9个关联关系）比重构前（12个）少。这将促进SAAT应用程序的可扩展性PSM_DBCreate = DBCreate？x的！return（）！DBCreate_r！创造！PSM_DBCreateParser_r！parse！PSM_解析器PSM_Parser =解析器？x的！parse（）！PSM_DBFill = DBFill？x的！fill（）DBFill_r！加油！PSM_DBFillPSM_DB_K = DB_K？x的！checkK（）！PSM_Analyse =分析？x的！return（）！Dobbankk_r！检查！PSM_DBBKKAnalyse_r！分析！PSM_分析StatCalc_r！计算！PSM_StatCalcPSM_StatCalc = StatCalc？x的！calculate（）！PSM_StatFilter = StatFilter？x的！filter（）！PSM_Saat =（DBCreate！创造！DBCreate_r？x的！StatFilter_r！过滤器！PSM_StatFilter解析器！parse！ Parser_r？x的！DBFill！加油！DBFill_r？x的！德贝莱克！检查！ DBBARK_r？x）！分析！分析！ Analyse_r？x的！快点！处决！Stat_r？x的！SKIPPSM_DB =（DBCreate！创造！DBCreate_r？x的！解析器！parse！ Parser_r？x的！DBFill！加油！DBFill_ r？x的！德贝莱克！去死吧！DBChecK_r？x）！停止PSM_Stat = Stat？x的！StatCalc！计算！StatCalc_r？x的！StatFilter！过滤器！StatFilter_r？x的！Stat178B.本·阿马尔，麻省理工学院布里和11.图11重构后的DB状态机图。图8重构前Saat的状态机图。图9重构后的类图图12使用FDR2进行验证。6.4. 模式正确性在重构之后，我们必须检查SAAT系统的行为保留。因此，我们遵守上一节所述的验证规则。图10重构后的Saat状态机图此外，Saat和DB的状态机图级别上的修改如图1和2所示。 10此外，重构后生成的Saat状态机图比重构前显示的状态机图要小。这种宣传将增强对SAAT应用程序行为方面的理解。与其他类对应的状态机图保持不变。PSM_Saat_r = DB！处决！DB_r？x的！分析！分析！ Analyse_r？x的！快点！处决！ Stat_r？x的！SKIP解析器！parse！ Parser_r？x的！DBFill！加油！PSM_DB_r= DB？x的！DBCreate！创造！ DBCreate_r？x的！DBFill_r？X！德贝莱克！检查！ DBBARK_r？x的！ DB_r！处决！DB引入关联关系的基于模式的模型重构179v使用FDR22，我们很容易证明Saat和DB之间要添加的关联关系的一致性，由以下两个断言表示：assertPSM_DB_rvsPSM_DBassertPSM_Saat_rsPSM_Saat这些断言由FDR2检查（见图2）。 12）。7. 结论重构是一种众所周知的提高软件质量的技术，特别是在可扩展性、可重用性和效率方面。它经常应用于代码。重构技术的核心问题在于重组过程执行之后的优先级保存。本文倡导在软件开发的高级阶段应用重构技术。将本文提出的引入关联关系的重构模式应用于类图、OCL约束和状态机图，可以得到高质量的UML模型，即正确的、可扩展的、可重用的和有效的UML模型。在这方面，作者（BenAmmar，2012）以前提出了其他重构模式，允许：1. 引入继承的概念2. 引入重新定义的概念3. 抽象类的概念介绍。4. 介绍多态性的概念。5. 介绍授权的概念（Ben Ammar等人， 2008年）。6. 泛型类的概念介绍上面提到的重构模式列表是基本的。它涵盖了继承、关联、多态、委托、抽象类和泛型类的概念的介绍。进一步的研究，其中一些目前正在我们的实验室中进行，需要进一步扩展，elucidate和详细说明我们提出的重构模式列表。还需要进行额外的工作来调查重构与分析或设计模式之间的关系，特别是涉及GoF的那些（Gamma et al.，1995年）。事实上，现有的UML模型可以通过重构操作来改进，重构操作引入了设计或分析模式。这个目标可以通过组合现有的重构模式来实现。（见图。第一章致谢作者谨向突尼斯斯法克斯科学学院英语语言组的AnouarSmaoui先生表示诚挚的感谢，感谢他提供的宝贵的语言编辑和润色服务。引用Abrial，J.R.，一九九六年。B书-北京大学出版社.Allem，K.，Mens，T.，2007年 Refactoringdes mode`les：conceptsetde`fis.输入：程序IDM 2007年。 赫尔墨斯科学出版社，拉瓦锡。2我们稍微修改了我们的规范CSP，以便它被接受FDR2Baumeister，H.，韦伯，B.，2013.软件工程和极限编程中的敏捷过程。在：第14届国际会议，XP 2013。施普林格出版公司，奥地利维也纳，2013年。Behm，P.，Benoit，P.，Meynadier，J.M.，1999. METEOR：B在大型项目中的成功应用。综合形式化方法，IFM99。LNCS，vol.1708年Springer Verlag，pp. 369-387.本·阿马尔，B.，2012年。RaffinementetRefactoringdespe′cificationsUML：Contributiona`l'inge 'nierie des systmes （ PhD thesis ） .EditionsUniversitairesEurope ee'ennesEUE.本 · 阿 马 尔 ， B. ， Bhiri ， M.T. ， Benhamadou ， A. Pattern derafnement：Introductionclasse中间日l级per.In：Confe'renceenInge'nieriEduLogiciel（RennesFrance，2012）.本·阿马尔，B.，Bhiri，M.T.， Souquie`res，J. 这是一个基于平等概念的事实上的阶级斗争。In：7e`meateliersur 厄齐， 库普莱阿韦茨乐XXVIe`me《信息技术》（法国枫丹白露，2008年）。Correa，A.，Werner，C.，2007.重构对象约束语言规范。软件系统模型6（2），113-138。Dijkstra，E.W.，1975.保护命令，不确定性和程序的形式推导。Commun. ACM 18（8），453-457。Einarsson，H.，Neukirchen，H.，2012.使用模型到模型转换同步重构uml图和模型的方法和工具。收录于：第五届重构工具研 讨 会 论文集， WRT '12。 ACM ， New York ， NY ，USA，pp. 16比23工程，C. S.，2009. Atelier B 4 -用户手册，版本4.0. Fowler，M.，1999.重构：改进现有设计代码. Addison-Wesley，Boston，MA，USA.伽马，E.，赫尔姆河，约翰逊河，Vlissides，J.，1995.设计模式。Addison-Wesley，Boston，MA.戈德史密斯，M.，2005年FDR2用户Gorp，P.，Stenten，H.，Mens，T.，Demeyer，S.，2003.走向自动化源代码一致的UML重构。在：Stevens，P.，Whittle，J.，Booch，G.（编），UML 2003-统一建模语言，计算机科学讲义，卷。2863号Springer-Verlag，pp. 144- 158霍尔，C.A.R.，2004.通信顺序进程。电子版由Jim Davies编辑。Idani，A.，Ledru，Y.，Labiadh，M.-A.Inge'nieriedirigeparlesmode`lespour une intgration efficace de uml etb.见：INFORSID 2009（图卢兹，2009年5月）。I fill，W.， Schneider，S.A.， Treharne，H.， 2007. 增强B带控制注释。In：Julliand，J.，库奇纳连科岛（编），计算机科学讲义，第4355卷。施普林格，pp. 34比48拉洛河 Concepti onetde′applime ntformelsd'applic a tions basesde donn e ′ es （PhD thesis ） . CEDR I C（CNAM），埃夫里大学，2002年。我不想做研究。Lano，K.，克拉克，D.，Androutsopoulos，K.，2004. UML toB：面向对象模型的形式化验证。In：IFM，pp. 187-206.Ledang，H.，2001年从UML规范自动转换为B.ASE'01 ： Proceedingsofthe16thIEEEInternationalConferenceonAutomatedSoftwareEngineering.IEEEComputerSociety，p. 四百三十六Ledang，H.，Souquie`res，J.，2002年。 UML和B规范技术的集成：从OCL表达式到B的系统转换。APSEC '02：第九届亚 太 软 件 工 程 会 议 论 文 集