电子笔记在理论计算机科学50第3期（2001年）。GT-VMT 2001网址：http://www.elsevier.nl/locate/entcs/volume50.html9页可视化模型Rei koHe ckel1JochenM. Ku第二节部数学与计算机科学学院德国帕德博恩D-33095摘要在本文中，我们讨论了在UML中的行为模型的一致性问题，目前的技术，指定和分析一致性。使用元模型规则，我们将UML模型的元素转换为语义域。然后，可以使用语言和工具指定和验证一致性约束语义域的一部分。这个一般的方法是由协议状态图继承的问题。关键词：Meta建模，模型验证，行为一致性1引言作为一种通用的建模语言，UML [11]缺乏在开发过程中如何使用某些图的精确相反，提供机制来定义领域或项目特定的专业化和方言（称为proles），并且每种方言可以具有其自己的方法。因此，不同图或子模型之间的语义重叠不能一劳永逸地解决，而是取决于所讨论的方言。在某种程度上，用于定义UML的抽象语法和静态语义的Meta建模方法[10]可以用于指定与UML方言相关的附加语法元素和结构一致性约束。然而，到目前为止，还没有一个通用的（即，Meta级）技术，用于指定UML及其方言的行为一致性。部分得到ESPRIT工作组APPLIGRAPH和TMR网络GETGRATS。1 电子邮件地址：reiko@upb.de2 电子邮件地址：jkuester@upb.dec2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。可观察的一致性。状态图继承的双重概念基于2向下GT-VMT2001{R. Heckel和J. Kuster下来2012年12月12日起来up up起来时间2014年4月3日下来ch1CH2下来prog12002年起来下来起来起来下来时间起来2004年第三章下来CH4CH3图1.一、Invocable behavior：电视的例子本文的目的是概述一种可视化模型行为约束的指定和验证方法。我们分四步进行。在（非正式地）确定了手头的一致性问题（第2节）之后，我们选择了一个支持我们感兴趣的一致性问题的语义域，并定义了一个模型到语义域的映射（第3节）。然后，我们使用语义域提供的语言和工具来制定行为约束并对其进行验证w.r.t.个人模型（第4节）。在本文的其余部分，我们将讨论方法通过制定UML状态图继承的两个概念，通过基于规则的映射到CSP。2UML状态图和继承在UML中，状态图可以与类相关联，以指定对象的生命周期，即，在该类的对象的生存期内调用该类对象的操作顺序。给定一个类A和A的子类B，相关状态图的行为一致性引起了状态图继承的问题。在文献中，提出了不同的概念（参见，例如，[3，2，7]）。在本文中，我们将把自己限制在与状态图的两种双重解释相关的两个概念上，这两种解释指定了可调用或可观察的行为。不可言的一致性。这种状态图继承的概念是基于替换原则的，该原则要求在需要A类对象的地方可以使用B这意味着，在超类上可调用的任何操作序列也可以在子类上调用例如，考虑图1中描述的情况。在这里，在Tv对象上调用的任何操作序列也可以在TvRemote对象上调用，因为前者的状态图完全包含在后者的状态图中[3]。ch1ch2ch3ch4电视遥控器起来停机时间电视3GT-VMT2001{R. Heckel和J. Kuster结婚单个结婚离婚生日生日单个盖茨基结婚无标记的接合结婚生日生日离婚生日图二.可观察行为：Person示例一个状态图被解释为方法调用的可观察序列的描述（上限）的想法。因此，每个关于子类的可观察序列必须导致（在已知方法的投影下）其超类的可观察序列。作为一个示例，请考虑图2凡 过滤掉getslogan方法，则会导致异常Per的行为，子对象可以被投影到Person对象上[3]。3抽象语义与指称语义Meta模型。我们作为示例使用的UML图的抽象语法由图3中的Meta模型指定 它定义了一种简单的状态图概念及其与阶级的联系。此外，泛化（类之间）被建模。表示符合UML Meta模型，但注意到一些继承关系和一个派生属性事件的引入，该事件应包含属于CompositeState内部转换的所有事件的集合。所有的Meta类都包含一个元属性name：string，图中没有显示。(In UML Meta模型（这是从超类ModelElement继承的）。CSP作为语义域。通信顺序进程（CSP）[8]提供了一个基于简单编程符号并由工具支持的并发数学模型[5]。事实上，语言和工具支持的存在接下来，我们简要回顾一下我们正在使用的CSP进程的语法和语义。给定一组动作A和一组进程名N，人生日聚会结婚聚会离婚隐私政策4源StateVertex1事件0.. 1触发子顶点目标过渡内部泛化父母11子女上下文伪状态类型：PStateKind国家前0名110.. 1CompositeStateisConcurrent：Bool events：SetSimpleStateFinalStateStateMachine类GT-VMT2001{R. Heckel和J. Kuster图三. UML Meta模型片段：协议状态图和一般化由P：：= stop j a！ P j P u P j P 2 P j P n a j pn其中a2A，A1 A，和pn2 N。过程名称用于使用方程pn = P来定义递归过程。业务之诠释如下。stop表示非活动（死锁）进程。 前x处理a！ P执行动作a并像P一样继续。过程PuQ和P2Q分别表示P和Q之间的内部选择和外部这意味着，当Pu Q演化为P或Q时，它执行的是一个内部的（-）动作，而对于P2Q，这需要P或Q的一个可观察的动作。例如，（a！ P）u（b！Q）执行，以便成为一个！P或B！Q. 相反，（a！ P）2（b！Q）必须执行a或b，并分别演化为P或Q。这种区别与下面状态图的翻译有关最后，进程Pn a的行为类似于P，只是所有的动作a都是隐藏的。CSP的语义通常根据跟踪和故障来定义跟踪就是进程执行时可以观察到的一系列动作。此外，失败（s; A）还提供了一组动作，这些动作可以在执行s之后被进程拒绝。过程的轨迹总是在压力下闭合因此，它们只能捕获过程的安全属性，即，对非活动进程也有效的属性停止。此外，故障模型可以捕获生命力条件，如无死锁。与这两个语义模型一起出现的是两个过程重构的概念nement。 我们写Pv T Q如果T（Q）T（P），即，Q的每一迹也是P的一迹。类似地，如果Q的失效包含在P的失效中，则P v F Q。一般来说，这个想法是，如果P比Q更确定（更少指定），则P是Q的元素。应使用这些关系来表达一致性要求。将状态图映射到CSP。状态图到CSP过程的转换5：国家名称= s：GT-VMT2001{R. Heckel和J. Kuster名称=鳍：FinalState：伪状态：国家状态（鳍）=停止状态= behState（comp）=State（default）（一）（二）（三）源：过渡X触发：事件名称={e1... en}（五）beh（s）：：=directBeh（s）[]beh（comp）（六）directBeh（s）：：=event（e1）【】……[] event（en）name = initkind = initial源name = default目标：过渡beh（s）：：=停止（四）源：过渡目标name ={s1... sn}触发（七）event（e）：：=e −>状态（s1）|~|......这是什么？|状态（sn）|State(sn)见图4。状态分解（1-3）和行为（4-7）由图4中的规则基于图3中的Meta模型进行描述。战略如下。首先，规则（1）到（3）创建了一个递归方程系统，每个递归方程系统对应于Meta类State的每个实例。其次，规则（4）至(7)用于替换所有出现的辅助进程名beh（在规则（2）中引入）由相应的过程定义。一般来说，所有以斜体设置的名称表示必须替换的“非终结符”注意，我们使用了机器可读版本的CSP表示法，其中[]和|~|分别表示2和u。注意规则（6）和（7）包含多个对象（由阴影边界表示），它们表示具体对象的最大集合因此，它们的属性提供了一组值，在我们的例子中是满足结构要求的所有事件fe 1;：; eng或状态fs 1;：;sng的名称集下面显示了这些规则对类Tradition- alPerson的状态图的应用。（类的名称缩写为TP。）请注意，（*）beh（single）= directBeh（single）[]beh（top）= beh（top）= STOP符合规则（5，4，6）和CSP公理p2STOP = p。这意味着，隐式top状态的外部行为（在具体语法中不可见，并且没有传出转换或超状态）是空的，对于也没有传出转换的statesimple也是如此。因此，规则（3）将状态single的语义定义为默认状态notengaged的语义。由于notengaged是SimpleState，因此应用规则（2）和（5）。在使用（*）删除超状态组件之后，我们只使用规则（6）和（7）收集传出的转换。订婚和已婚的语义也是以类似的方式计算的。：StateMachine名称=组件：CompositeState名称= e：活动名称= s：国家名称= s：国家name = compisConcurrent = falseevents = E：CompositeState颠覆：StateVertex名称= s顶部：国家名称= s6：StateMachine：StateMachine顶部：国家name =top2events = E2孩子上下文名称= C2：类泛化GT-VMT2001{R. Heckel和J. Kuster顶部：国家name =top1events = E1图五、泛化的限制。Invocableconsideration：C2（top2）vT C1（顶部1）。可观察到的一致性：C1（前1）vT C2（top2）n（E2E1）.TP（单次）= TP（未测量）（3）TP（notengaged）= beh（notengaged）（2）= directBeh（notengaged）[]beh（single）（5）= directBeh（notengaged）（）= event（birthday）[]event（getsday）（6）生日！TP（notengaged）[]获取！TP（engaged）（7）TP（engaged）= beh（engaged）（2）= directBeh（engaged）（5;）结婚了！TP（已婚）[]生日！TP（投入）（6; 7）TP（已婚）= directBeh（已婚）（2; 5;）离婚了！TP（notengaged）[]生日！TP（已婚）（6; 7）4行为约束规格。基于状态图到CSP的映射，可以制定第2节中讨论的状态图继承的两个概念的形式一致性条件。两者都使用图5的模式。为了捕捉可调用一致性的思想，即超类接受的每个方法调用序列也应该由子类实现，我们要求前者是后者的一个元素。（P v T） Q IT（Q）T（P））。如果超类的状态图表示子类的可观察行为的上界，则必须指定一个对偶条件，用n（E2E1）隐藏子类中新引入的所有操作.确认使用FDR工具，这种一致性约束可以是-上下文母名称= C1：类7GT-VMT2001{R. Heckel和J. Kuster图六、FDR工具的屏幕截图显示了一个反例分析过了关于可观察的行为，我们可以证明P（single）vTTP（single）n是可观察的。这意味着传统人的所有痕迹都包括在人的痕迹集中，其中隐藏了传统人的痕迹中未为人定义的操作关于方法的可调用序列，TP（ single ） 不 是 P （ single ） 的 一 致 性 元 素 ， 因 为 跟 踪 getsMarried 在AppropriationalPerson的实例上不可调用。对于Tv的例子，我们可以证明TvRemote（prog 1）vTTv（prog 1）。这意味着在Tv对象上调用的任何操作序列也是TvRemote对象的可调用序列。相反，TvRemote与Tv不明显一致，因为Tv（prog 1）vTTvRemote（prog 1）不能被建立。这是因为在TvRemote上可调用的跟踪up ch4 timeup的限制产生了跟踪up time up，它不是Tv的跟踪。图6显示了FDR工具的屏幕截图，展示了这个示例。该工具本质上是一个模型检查器，用于验证两个CSP表达式之间的关系。如果这个关系不成立，则产生一个跟踪或失败作为反例。很明显，为了使我们的方法可用，将需要一个接口，提出这样的反例在UML符号。8GT-VMT2001{R. Heckel和J. Kuster5结论在本文中，我们提出了一种方法，用于指定和分析可视化建模技术中的行为约束，模型映射到一个语义域的语言和工具支持的基础上。这种方法不限于行为一致性约束。例如，[6]基于转换成线性不等式系统来分析结构图中基数约束的一致性。另一种方法，也是基于解决线性不等式系统，是[9]谁分析时序图的时序约束。基于规则的映射，如第3节中的映射，也用于[12，1]，其中提出了时间Petri网作为UML的语义框架。然而，请注意，我们的目标不是为UML（甚至是它的合理的子语言）提供指称语义。相反，映射是针对感兴趣的语言特征本地定义的，即使其他模型元素的语义还不清楚。为了能够修改一致性的概念（当开发过程发展或创建新的prole时），重要的是这种映射是灵活和可扩展的。 我们认为，基于规则的概念已经在[4]中用于描述Java代码生成，最初是由成对语法[13]激发的，提供了一个很好的起点。然而，它必须得到一个能够从这种基于规则的描述中生成翻译器的工具的支持。目前，我们正在研究为此目的使用XSL转换。引用[1] 巴雷西湖和M. Pezz e，Improving UML with Petri nets，in：Proc. ETAPS2001 Workshop on Uniform Approaches to Graphical Process Speci cationTechniques（UniGra），Genova，Italy，Electronic Notes in TCS（2001），to appear.[2] Ebert，J. and G.恩格斯，OMT类的结构和行为观点，在：E. Bertino和S. Urban，editors，Proceedings，Object-Oriented Methodologiesand Systems，LNCS 858（1994），pp. 142{157.[3] Ebert，J. and G.恩格斯，《对象生命周期定义的规范》，1995年，《大学学报》Koblenz-Landau（1995）。网址http：//www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-19-95.ps.gz[4] Engels，G.，R. 胡cking，S. Sauer和A. Wagner，UML编译模型及其到Java的转换，载：R.法国和B. Rumpe，editors，Proc. UML'99，Fort Collins，CO，USA，LNCS1723（1999），pp. 473{488.[5] Formal Systems Europe（Ltd），\Failures-Divergence-Re nement：FDR 2用户手册，”（1997）。9GT-VMT2001{R. Heckel和J. Kuster[6] Fradet，P.，D. L. M etayer和M.多视图软件体系结构的一致性检验，O.Nierstrasz和M. Lemoine，editors，ESEC/FSE '99，Lecture Notes in ComputerScience1687（1999），pp. 410{428.[7] Harel ， D. 和 O. Kupferman ， On the Inheritance of State-Based ObjectBehavior ， Technical Report MCS99-12 ， Weizmann Institute of Science ，Faculty of Mathematics and Computer Science（1999）。[8] 霍尔角A. R.，\Communicating Sequential Processes，”Prentice Hall，1985.[9] Li，X.和J.Lilius，UML序列图的时序分析，在：R.法国和B. Rumpe，编辑，UML'99 -统一建模语言。超越标准。第二届国际会议，柯林斯堡，CO，美国，10月28日至30日。1999，Proceedings，LNCS1723（1999），pp.661{674.[10] 对 象 管 理 组 ， Meta 对 象 工 具 （ MOF ） 规 范 （ 1999 ） ，http://www.omg.org。[11] 对象管理组，UML规范版本1.3（1999），http：//www.omg.org。[12] Pezze， M.和L.Baresi，Can graph grammars make formal methods morehuman ？ ， in ： A. Corradini 和 R. Heckel ， editors ， Proc. ICALP 2000Workshop on Graph Transformation and Visual Modeling Techniques ，Geneva，Switzerland（2000），http://www.di.unipi.it/GT-VMT/.[13] Pratt ， T.W. ， Pair grammars ， graph languages and string-to-graphtranslations ， Journal of Computer and System Sciences5 （ 1971 ） ，pp.560{595.
我的内容管理
展开
