没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记152(2006)69-81www.elsevier.com/locate/entcs使用ATL检查模型1我是贝兹温·弗·德·埃里克·茹奥ATLAS集团、INRIA和LINA,法国南特大学{jean.bezivin,frederic.jouault}@univ-nantes. fr摘要使用模型通常需要能够断言给定模型对给定约束集的遵从性。 一些工具能够检查UML模型上的OCL不变量。 然而,很少有工具能够对任何元模型做同样的事情。这对于DSL(领域专用语言)模型工程方法来说是非常不利的。 在本文中,我们提出了一个元模型-使用ATL(ATLAS Transformation) 语文)。 这解决方案已被实现为基于插件的插件。关键词:模型工程,OCL,模型检查,ATL1引言模型工程是基于模型符合显式元模型的概念[4]。元模型约束模型的结构:模型的元素由其元模型的元素类型化然而,这在实践中往往不够需要具体说明其他限制比如说,如果一个元模型简单地将一个人的年龄属性定义为一个整数,则无效(例如,负的)值。为响应这一要求,OMG(对象管理组织)指定了OCL(对象约束语言)来表达模型上的约束。目前,UML [11]是最广泛使用的元模型,并得到大量工具的支持UML旨在对软件工件进行建模,并且可以通过使用profiles来适应特定领域OCL支持1 部分工作由ModelWare,IST欧洲项目511731支持。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2006.01.01570J. Bézivin,F.Jouault/Electronic Notes in Theoretical Computer Science 152(2006)69从一个UML工具到另一个。最先进的是能够评估(或编译)约束。但是模型工程不仅仅是关于UML的。DSL [6](领域特定语言)方法促进了大量小型领域特定元模型的定义,而不是使用单个大型元模型。目前,很少有DSL工具能够评估模型上的约束这项工作的目的是展示如何使用现有的模型转换工具,如ATL [2][1]。在[4]中,我们认为“一切都是模型”的原则在[2]我们通过证明模型之间的转换如何具体地被视为一个模型来追求这一点。在这里,我们试图更进一步地表明,验证本身也可以被同样地考虑。传统上,验证是从模型返回布尔值的函数。如果我们称f为验证函数,可以 记 为 f : Model→Boolean 。 约 束 可 以 从 f 中 以 特 定 类 型 的 Model :Constraints的形式提取,得到fJ:Model×Constraints→Boolean。为了指示 错误 的严 重性 级别 ,验 证的 结果 可 以扩 展为 一个 表 达式, 如fJJ:Model×Constraints→Bit。我们在这里提出另一种扩展,将结果视为一种特殊的模型:一个诊断,以获得FJJJ:模型×约束→诊断。本文的结构如下:第2节给出了一个示例DSL作为说明。在第三节中,我们分析了模型的良构规则的一些要求。第4节探讨使用模型来表示模型验证的结果。第5节展示了ATL如何用于检查模型上的约束。第6节介绍相关工作。2激励示例:类图在本文中,我们将使用一个非常简单的DSL,称为CD的类图。这是出于简洁的原因而选择的,但是可以类似地使用更复杂的DSL。图1给出了CD的元模型。CD可以被认为是UML的简化子集。类图中的每个元素都有一个名称。类可以有超类型和StructuralFeatures,它们是对其他类或属性的引用。StructuralFeatures具有多重性,并且由Class或DataType类型化。包用于通过对相关元素进行分组来构造图。图1中给出的定义显然是结构性的,但仍然不完整。因此,有可能创建符合CD的模型,但这些模型不是有效的类图。CD的规格可以通过添加J. Bézivin,F.Jouault/Electronic Notes in Theoretical Computer Science 152(2006)6971Fig. 1.一个简单的类图元模型两个约束(C1)和(C2):类名称在包中必须是唯一的(C1),结构特征名称在类及其超类型中必须是唯一的(C2)。CD的完整定义将在某个地方进行,并且超出了本文的范围。我们更愿意将自己限制在少数约束中,包括(C1)和(C2)。重点是给出它们的可用的具体表达。3模型工程中的良构规则为了自动验证,约束必须用一种可以自动翻译为可执行形式的语言编写这里使用了著名的OCL解决方案.在本节中,我们通过添加严重性和描述来扩展简单的OCL约束。结果可用于指定模型的良构规则。3.1使用OCL表示约束OCL基本上知道三种约束。不变量必须在任何时候都被验证,模型应该处于一致的状态。前置条件和后置条件是在操作中指定的,并且必须分别在其主体执行之前和之后有效只有一些元模型具有执行语义,因此需要这样的约束。由于这不是一般情况,我们将只考虑第一类约束不变量在元模型类型的上下文中定义。它由一个布尔表达式组成,对于这种类型的每个元素,该表达式的值必须为true。图2给出了(C1)和(C2)的OCL规格。Class上的allStructuralFeatures()操作返回所有72J. Bézivin,F.Jouault/Electronic Notes in Theoretical Computer Science 152(2006)69--(C1)错误:分类器的名称必须--在其包装中是独一无二的。context分类器inv:not self.package.contents->exists(e|(e<> self)和(e.name =self.name))--(C2)错误:StructuralFeature的名称必须--在它的类和超类型中是唯一的。contextStructuralFeature inv:not self.owner.allStructuralFeatures()->exists(e|(e<> self)和(e.name =self.name))图二. 将(C1)和(C2)表示为OCL不变量属于类及其所有超类型的StructuralFeatures。它也可以在OCL中定义,如附录(第8节)所列3.2向约束对于每个CD模型,必须验证两个不变量(C1)和(C2)。然而,有时指定不应违反的约束是有用的当这些约束没有得到验证时,模型的一致性就不会被证明是错误的。这与编译器传统上将消息标记为错误或警告的方式非常相似。错误是致命的,而警告则表示存在潜在问题。我们将在下面的段落中看到,在这个标度中可以定义更多的度数。我们现在将把这称为约束的严重性。根据这个定义,(C1)和(C2)是错误的,因为违反它们的模型不是有效的类图。让我们考虑以下两个约束:在类图中,抽象类应该有子类(C3),类的名称应该以大写字母开头违反(C3)或(C4)的CD模型仍然是类图。因此,这些约束不是错误。与非错误约束相关联的精确在这个例子中,我们认为(C3)是一个警告,因为在某些编程语言中无法访问代码(C4)在这里被称为批评者,因为它不是错误,并且根本不影响元模型的结构。这只是一种风格上的考虑。图3给出了这两个约束的OCL表达式。3.3向约束到目前为止,对不变式的违反只能与约束本身、其严重性和违反模型元素相关联。然而,并不总是J. Bézivin,F.Jouault/Electronic Notes in Theoretical Computer Science 152(2006)6973--(C3)警告:抽象类应该有子类。context类inv:not(self.isAbstract and(Class.allocation()->select(e|超类型->包含(self))->size()=0))--(C4)Critic:分类器的名称应该--以大写字母开头。context分类器inv:not(let firstChar:String=self.name.substring(1,1)infirstChar<> firstChar.toUpper())图三. (C3)和(C4)作为OCL不变量self.nameself.owner.name’The图四、当与(C2)关联时,OCL表达式评估为上下文适应的错误消息很容易理解这个问题,只有与约束相关联的布尔表达式。因此,应将描述与每个约束相关联。 对于图2中的(C1)和(C2)以及图3中的(C3)和(C4),已经以注释的形式然而,这还不够,因为工具不能使用这种自由形式的规范。在UML中,约束有一个名称,可以用来粗略地指示约束的语义,作为人类可读的字符串。这是第一步。 但在某些情况下,消息的文本可能需要根据上下文进行调整。例如,它可以包含对违规元素的某些属性值的引用我们在本文中使用的解决方案是将描述指定为一个计算为字符串的OCL表达式。图中给出了一个例子4为(C2)。然而,由于诊断是一个模型,如果有必要,可以生成问题的更精确和结构化的表示3.4扩展OCL正如我们之前所观察到的,工具需要访问约束的严重性和否则,图3中给出的规格无法与图2中给出的规格区分开来。因此,OCL需要扩展来支持附加到约束的其他元素。图5给出了(C1)的扩展版本,除了其74J. Bézivin,F.Jouault/Electronic Notes in Theoretical Computer Science 152(2006)69上下文CD!分类器报告错误self.name’agetLocation()如果self.package.contents->存在(例如|(e<> self)和(e.name= self.name));图五. (C1)的具体化和OCL扩展上下文及其布尔表达式:• 严重性,指示问题的失败程度这是一个错误,但也可能是一个警告或批评,例如。• 描述,以人类可理解的方式陈述问题。请注意,使用了一个动态构建的字符串,该字符串使用了违规元素的名称• 在计算机可读格式中对问题位置进行编码的字符串。要使用的格式的选择取决于工具,可以在getLocation()操作中实现。4将验证结果表示为模型模型上的一组约束会导致诊断。在本节中,我们考虑诊断的几种表示,并给出一个示例元模型。4.1诊断学的不同表示最简单的诊断形式是布尔型。true值意味着模型满足所有约束,而false值意味着模型无法满足所有约束其中如果诊断被表示为整数,则其可用于对故障程度进行编码。例如,它的值可以是违反约束的次数,可选地由每个约束的严重性加权这有点有趣,但对于指出问题的性质和位置没有很大帮助需要更复杂的表示一些工具以文本方式(例如编译器)向用户呈现因此,诊断的结构被明确指定为元模型。由于诊断是一个模型,因此可以对其执行任何转换例如,使用模板“在IDE中,诊断J. Bézivin,F.Jouault/Electronic Notes in Theoretical Computer Science 152(2006)6975见图6。 Eclipse原型模型可以被映射到本地表示(例如,Eclipse中的IMarkers然后问题会显示在编辑器和“Problems”视图中的相应位置还可以导出诊断的许多其他表示。4.2诊断的元模型一个元素可以通过或失败约束的验证。第一种情况被认为是正常的,不需要记忆。在第二种情况下,已经发现了问题。图7的元模型指定了一个Problem类来表示这样的问题。当一个模型的评估产生一个空的问题模型时,它满足了一整套约束每个Problem都具有与约束相关联的严重性(使用枚举类型)它还包含一个描述和一个位置,由字符串表示。严重性级别的数量以及问题的位置和描述的表示可以进行调整以适应特定需求。76J. Bézivin,F.Jouault/Electronic Notes in Theoretical Computer Science 152(2006)69见图7。用于诊断的示例元模型:问题5使用ATL引擎验证约束5.1ATL介绍模型转换是从一组源模型自动生成一组目标即将到来的OMG模型转换标准称为QVT [10](查询/视图/转换)。ATL是一种类似QVT的模型转换语言。ATL的执行引擎在GMT网站上以开源(EPL许可证)Eclipse插件集的形式提供[7]:执行引擎,转换编辑器,源代码级调试器等。ATL是声明式和命令式的混合体。本文件只对声明部分感兴趣以下定义仅描述了ATL的一个子集了解接下来会发生什么。ATL转换程序由转换规则组成。每个规则都包含一个要在源模型中匹配的源模式和一个要在目标模型中为每个匹配创建的目标模式源模式有一个来自源元模型的类型和一个以OCL布尔表达式形式存在的保护规则的匹配对应于源模型的元素,该元素由规则的源模式类型键入,并且针对该元素,防护评估为真。目标图案由一组来自目标元模型的类型每个类型都与一组绑定,每个绑定指定如何从OCL表达式初始化它的一个属性对于规则的每个匹配,在目标模型中为每个目标模式类型创建一个元素然后通过应用相应的绑定来初始化每个目标元素。5.2约束的ATL表示ATL引擎只能用于验证约束,如果它们被表示为刚才指定的。从一组约束创建检查程序的算法如下:对于每个约束,创建ATL转换规则,以便:• 规则的源模式类型是约束的上下文。• 规则的保护包含布尔表达式的否定,如-J. Bézivin,F.Jouault/Electronic Notes in Theoretical Computer Science 152(2006)6977见图8。 验证者与约束有关。请注意,我们在图2中将(C1)和(C2)以及图3中将(C3)和(C4)表示为否定(即形式为not expr>)。 我们确实预料到双重否定会消失,从而产生一个更简单的程序。• 规则的目标模式指定了一个类型:问题,它将在匹配时创建(即,(一)违反不变量)。• 它将使用三个绑定进行初始化:不变式的严重性,问题的描述及其位置。由于目标元素是从导航源模型的OCL表达式初始化的,因此将描述实现为构造的字符串是简单的。在附录(第8节)中给出了实现(C1)、(C2)、(C3)和(C4)解决方案的ATL转换的源代码我们使用Eclipse建模框架[5]在Eclipse插件中实现了对CD模型上一组稍大的约束的我们选择使用简单的语法以文本形式表示在这种情况下,因此,问题由一行和一列编号组成。图6示出当类图包含问题时,实际上呈现给用户的是什么5.3解决方案分析图8给出了约束验证的通用结构。验证者检查模型上的约束,这导致诊断。让我们注意V是验证者执行的操作,M是要验证的模型,C是约束,D是结果诊断。我们可以写D=V(M,C)。我们刚刚提出了一个解决方案,将约束和验证器集成在同一个实体中:ATL程序。如果我们把P记在这个程序上,那么我们有D=P(M)。通过比较D的两个表达式,我们观察到P对应于V,其中C已经被求值。这与函数式语言的currying操作事实上,咖喱V的值不应是V C (M),满足D=VC(M)。一组给定的约束C很可能被用来检查几个模型是否符合相应的元模型。不必每次都重新评估所有约束这就是我们在实际中使用ATL编译器编译约束时所做的78J. Bézivin,F.Jouault/Electronic Notes in Theoretical Computer Science 152(2006)696相关工作这篇论文中提出的工作与代码气味的概念有关[8]。气味表示代码中有问题的片段。这个概念可以适用于模型。因此,在[12]中,作者展示了如何使用OCL表达式在UML模型上指定这种气味利用本文提出的解决方案,可以对不同类型的模型进行代码气味评估气味的检测可以在OCL中实现,使用这种语言的所有功能(迭代器,递归等)。气味检测器的目标元模型可以适应现有的工具。ATL引擎可以用来检测特定的代码气味。气味的概念经常与重构的概念联系当在模型上检测到气味时,可以采取适当的措施来解决问题。这种重构也可以作为模型转换来实现。因此,这里所介绍的工作展示了如何实现一个完整的自动化重构链7结论和今后的工作我们提出了三个改进模型工程中约束检查的建议:• 约束在OCL中有一个上下文和一个布尔表达式,与附加信息相关联。例如,这可以是严重性、描述、位置等。• 对模型上的一组约束条件进行验证所得到的诊断结果被认为是一个模型。这个模型可以被转换成任何表示形式:文本、图形、嵌入GUI等。• ATL语言可用于表示模型上的约束然后使用ATL编译器编译它们,并使用ATL引擎执行验证。这种方法可以用于任何元模型和多种上下文中。例如,验证UML模型相对于给定概要文件的有效性另一个可能的用途是保护模型转换的执行事实上,转换程序经常对它们的源模型做一些假设,这些假设不是它们的元模型的一部分 通过首先执行检查程序,用户可能会被警告不正确的转换使用。该方法也适用于模型上度量的计算。需要扩展目标元模型以支持所需的结果表示。OCL表达式可用于指定J. Bézivin,F.Jouault/Electronic Notes in Theoretical Computer Science 152(2006)6979来计算度量。然后将这些表达式嵌入到ATL转换中。在所有这些情况下,复杂的关系网出现在元模型、UML概要文件、通用转换、约束检查转换等之间。megamodel [3]的概念是处理这种额外复杂性的可能解决方案引用[1] ATLAS组,ATLAS转换语言,参考站点:http://www.sciences.univ-nantes.fr/lina/atl/网站。[2] B'ezivin , J. , Dup'e , G. , Jouault , F. , Pitettte , G. 和 Rougui , J. E. ,Firsteperrimentswiththe ATL model transformation language : Transforming XML intoXQuery , 2nd OOPSLA Workshop on Generative Techniques in the context of MDA ,Anaheim,CA,USA(2003).[3] B'ezivin ,J. ,Jou ault,F. ,Val dur i ez,P. ,OOPSLAWork shoponBest Practices forModel-Driven Software Development,Vancouver,BC,Canada(2004).[4] B'ezivin,J. ,Otheunicationpoweroffmodels,SoftwareanddSystemsMo delingg,第4卷,第2期,2005年5月,第171 - 188页。[5] Budinsky,F.,Steinberg,D.,Raymond Ellersick,R.,Ed Merks,E.,布罗德斯基,S。一、格罗斯,T。J.,“Eclipse Modeling Framework”, Addison Wesley[6] Czarnecki,K.,Eisenecker,U.,“Generative Programming: Methods, Tools, and Applications”,Addison-Wesley[7] Eclipse基金会,http://www.eclipse.org/gmt/网站。[8] Fowler,M.,“重构-改进现有代码的设计”,Addison Wesley,1999年7月。[9] OMG,http://www.omg.org/docs/ptc/03-10-14.pdf网站。[10] OMG,请求提案:http://www.omg.org/cgi-bin/doc? ad/2002-4-10。[11] OMG,http://www.omg.org/docs/ptc/03-08-02.pdf[12] Van Gorp, P. ,Stenten ,H. ,Mens, T.,Demeyer, S.,Towards automating source-consistent UML refactorings,In Proceedings of UML 2003 Conference,Springer-Verlag LNCS2863,San Francisco,CA,October 2003,pages 144 - 158.8附录- 验证(C1),(C2),--CD(即类图)模型上的(C3)和(C4)。模块CD_Verifier;80J. Bézivin,F.Jouault/Electronic Notes in Theoretical Computer Science 152(2006)69从IN: CD创建 OUT:Problem;--(C1)错误:分类器的名称必须--在其包装中是独一无二的。ruleClassifierNameUniqueInPackage {从i:CD!分类器(即包.内容->存在(e|(e<>i)和(e.name= i.name)到问题!问题(location- i.location,severity- Severity::error,description-i.name’already)}帮助上下文CD!类定义:allStructuralFeatures():Sequence(CD!StructuralFeature)=self.structuralFeatures->union(self.supertypes->collect(e|e.allStructuralFeatures())->flatten());--(C2)错误:StructuralFeature的名称必须--在它的类和超类型中是唯一的。ruleStructuralSystemName UniqueInClass {从i:CD!结构特征(letsfs:Sequence(CD!StructuralFeature)=i.owner.allStructuralFeatures()insfs->exists(e|(e<>i)和(e.name = i.name)到o :问题!问题(location- i.location,severity- Severity::error,description-i.owner.namei.name’)}--(C3)警告:抽象类应该有子类。J. Bézivin,F.Jouault/Electronic Notes in Theoretical Computer Science 152(2006)6981rule AbstractClassShouldHaveChildren{ fromi:CD!类(i.isAbstract和(CD!Class. allocation()->select(e|例如,超类型->包含(i))->大小()= 0))到o :问题!问题(location<- i.location,severity<- Severity::warning,警告-<'th e abstrac t Cla s ' + i. NAME+’ 没有孩子)}--(C4)Critic:分类器的名称应该--以大写字母开头。rule ClassifierNameShouldStartWithUpperCase{ fromi:CD!分类器(let firstChar: String= i.name.substring(1,1)in firstChar<> firstChar.toUpper())到o :问题!问题(location<- i.location,severity<- Severity::critic,description<-i.name’)}
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- zigbee-cluster-library-specification
- JSBSim Reference Manual
- c++校园超市商品信息管理系统课程设计说明书(含源代码) (2).pdf
- 建筑供配电系统相关课件.pptx
- 企业管理规章制度及管理模式.doc
- vb打开摄像头.doc
- 云计算-可信计算中认证协议改进方案.pdf
- [详细完整版]单片机编程4.ppt
- c语言常用算法.pdf
- c++经典程序代码大全.pdf
- 单片机数字时钟资料.doc
- 11项目管理前沿1.0.pptx
- 基于ssm的“魅力”繁峙宣传网站的设计与实现论文.doc
- 智慧交通综合解决方案.pptx
- 建筑防潮设计-PowerPointPresentati.pptx
- SPC统计过程控制程序.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功