网址：http://www.elsevier.nl/locate/entcs/volume51.html13页作为统一框架的Institutfu柏林理工大学软件与技术与信息工程学院，德国在第四节，塞克。 FR6{1，FRanklinstr. 28/2910587柏林，德国MartinGro e{Rhode1;2摘要基于图重写的软件系统规范有多种不同的方法。为了将这些和其他基于状态和/或规则的方法联系起来，已经引入了代数变换系统。 它们构成了一个语义域，独立于图或代数的重写被定义（实现）的方式。组合操作和关系已被定义为代数转换系统，以这种方式产生一个全面的语义规范框架。不同的图重写方法中的重写、转换系统、组合和元素等相应概念可以与这些语义概念进行比较，从而将它们联系起来，展示它们的兼容性。1引言已经提出了许多不同的用于图和图类结构的转换的形式主义，它们产生了各种软件系统的基于状态的形式模型（在[17，5]中给出了一个综述）。它们支持基于规则的规范方法，因为规则集是作为系统行为的规范给出的。每种特定的图转换方法都定义了规则何时以及如何应用于图（或用于表示系统状态的任何结构）以及如何转换图。因此，以这种方式定义的动态行为既取决于实际状态，因为它们确定哪些规则是适用的，又取决于规则，因为它们确定状态如何改变。显然，一个规范的语义在很大程度上取决于在规范中如何准确地定义规则的适用性和效果。例如，被删除的节点的上下文会发生什么变化1http://tfs.cs.tu-berlin.de/管理员2电子邮件地址：mgr@cs.tu-berlin.dec 2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2所有相邻边是否也被删除，和/或是否必须在规则中明确说明？如何解决删除和保留的冲突？在这些情况下，规则的应用是允许的还是禁止的？除了这些问题的答案之外，所提出的方法还在它们支持什么样的国家代表结构方面有所不同。简单图、超图、标记图、类型图、属性图和图结构只是一些常用的结构。当然，这也影响了该方法用于系统建模的方式。首先，因为系统状态必须在这种结构中表示，其次，因为状态和规则之间的相互作用决定了规范的形式语义，从而也影响了建模。因此，必须在一开始就做出建模决定，|由于不同方法之间缺乏过渡，|所选择的方法以后不能改变。比较的主要问题是，大多数方法都是基于转换的实现方式，即，规则应用的结果的构造（[14]的显著例外）。另一方面，描述性方法将使规范框架基于总体语义概念。这意味着，不是定义规则如何转换图，而是将第一转换系统定义为系统的正式语义模型，而与它们是如何构造的无关。在此基础上，通过定义模型，可以建立规范框架抽象规范意味着表达这种系统的属性，表示系统组件的组合的语义级别上的组合操作，也是在语义级别上的关系（或其他开发）关系，其支持从更抽象的设计或需求规范迭代开发更具体的设计规范。这意味着，语义是首先确定的。然后，可以分析和比较不同方法中的结构（图变换、组合和规格的关系）。的语义结构。在本文中，这种描述性的方法进行了讨论。它基于代数作为状态，这产生了一个非常全面和富有表现力的框架，以及表示系统步骤的一般代数变换。在下面的部分中，给出了代数转换系统的相应语义域，其中代数转换系统作为动态实体（系统、组件、对象等）的形式化模型，他们的抽象物种，阳离子手段、合成操作和发展关系。然后在第三节简要讨论了这种方法的一些应用。为了将代数变换系统的描述性方法与构造性图变换方法联系起来，在第二节中引入了代数变换规则作为代数重写规则的相应构造性解释四、3这意味着，变换规则，已被引入作为抽象规格- i-阳离子手段的意义上的公式描述的系统，也可以用来构造系统的状态，通过将它们应用到给定的状态（=代数）。文章最后给出了一个简短的结论2代数变换系统在一系列的论文（例如见[8，9]）中，代数转换系统已经被开发为上述意义上的语义框架。简而言之，可以描述如下。数据状态一个系统的数据状态被表示为一个任意签名的部分代数，由任意组的条件存在方程约束。这包含了所有类型的图，也允许使用n元部分函数和谓词。更重要的是，签名产生了一种语言（项、方程、公式）来表示系统中处于某种状态的元素，并推理其属性。状态变换状态变换由部分代数对给出，变换的开始和结束状态由代数的载体集上的关系族，通过状态变化跟踪元素的身份，一组被认为是转换步骤的可观察活动的动作实例。这些操作由一个额外的操作签名指定，该签名引入了它们的名称和参数类型列表。控制状态和转换转换系统的一个重要特征是数据状态和控制状态的区别。这意味着，系统的反应性（反应或行动的能力）不需要完全由数据的实际状态决定。相反，抽象的控制状态和转换作为一个（未标记的）转换系统单独给出。这些被标记然后由部分代数分别作为数据状态和代数变换。图1示 出 了 未 标 记 的转 换 系 统 （ 具 有 控 制 状 态 b; c; d; ： 和 转 换 t 1; t2;：：）：）用于选择数据状态（B; C、温度; D;：：：）以及系统进入并从所有部分代数的类执行的变换和经由标记的所有可能的变换，由虚线垂直箭头指示。（只有少数可能的数据状态和转换是4D_czb，t1，t3，，，，，，e_，z_c.˛t2，___玉米 栽培种JzFz.JzB， .J.J，E，z，z2zz_，JzG，s第二幕D，szH，szFig. 1.变换系统是具有状态和变迁标号显示明显。此外，仅对于转变t2示出了具有跟踪关系和动作集的完整变换。）性能规格变换系统的性质可以根据其结构进行分类。数据不变量，即，必须在每个状态下保持的属性可以被表示为条件方程（或其他公式）w.r.t.表示数据状态的代数的给定符号检查其有效性w.r.t. 代数 也包括单个状态的属性，如初始化或同步所需的初始化条件或属性属于此类。单个步骤的转化行为，即，数据状态改变的方式由变换规则表示这些由描述变换的开始和结束状态的成对方程组L和R以及具有形式参数x1;：;xn的动作表达式a（x1;：：;xn）给出，该动作表达式指定哪些动作实例对应于步骤。从而检查转换规则的有效性w.r.t. 转变系统的全局控制流行为可以以不同的方式指定（该方法是通用的w.r.t. 用于控制的指定方法行为）。像时态或其他模态逻辑这样的逻辑形式主义规范了标记转换系统的集合，并且也可以用于转换系统的规范。像进程演算、Petri网或状态图这样的方法指定了单个标记的转移（或转换）系统。这些全球控制流规范的有效性检查w.r.t.整个转换系统。合成运算转换系统的组合操作分两步定义。首先，必须连接应组成的转换系统。这是通过在它们的5转移系统以及它们的数据状态和动作的识别关系。前一种状态可以在组合系统的一个步骤中一起执行，并且在它们可以一起形成一致的全局系统状态的意义上，这些状态是同步的。标识关系表示数据状态的哪些部分是共享的（构建在静态数据类型、常用数据、共享变量等中）。以及共享哪些动作（互补输入/输出动作、发送/接收、握手等）。这种联系可以看作是系统的架构对于以这种方式连接的一组变换系统，定义了将组合系统再次表示为单个系统的组合结果。这意味着，它产生一个抽象视图，隐藏了组合系统的内部架构。它的控制状态和变迁分别由本地组件的同步状态和变迁元组给出。 它的数据状态（和跟踪关系）是本地数据状态w.r.t.识别关系及其动作集是局部动作集的并集。发展关系转换系统的发展关系是根据其底层转换系统的态射和其数据状态（部分代数）和动作集上的遗忘函子来定义的。 这些可以以不同的方式组合，从而产生不同种类的发展关系，如减少，扩展，隐藏和限制。此外，它们可以与闭包操作（如顺序（传递）或并行闭包）结合。这产生了进一步的关系或实施关系。注意，组合操作和关系在这里都被抽象地视为方案，可以以不同的方式实例化以分别获得具体的组合操作和关系。这些方案在[11]中有明确的定义。（在[20]中已经给出了LTS的类似分类分析，以比较流程规范的不同语义。）转换系统的组合的连接关系产生图，其极限（总是存在的）产生组合操作的结果（设计规范或时间理论的类似图表（跨度）已在[6，1]中使用，例如，用于确定组件的叠加和协调。）开发操作基于转换系统的态射。这也产生了主要的组合性结果：与其互连兼容的局部系统的每个发展步骤家族产生了（限制是函式的。）此外，还讨论了代数方程满足的不变性.签名的改变可以被推广到用于变换系统的类似满足条件以及仅涉及数据状态或变换的那些规范（所谓的数据空间属性）。这意味着，发展6保持数据空间属性，并且组合保持其组件的本地数据空间属性。全局控制由于对这些性质的规范方法的一般处理，一般不能预期低性能代数转换系统的范畴化处理也导致了进一步的推广，允许用其他机构的模型（抽象模型理论/规范框架，参见[7]）替换部分代数作为数据状态。这产生了一个非常灵活的规范框架，例如，具有对象引用和对象标识的面向对象系统的形式模型可以直接表示为具有链接的代数族（参见[12]）。作为一个全局性的结果，在[11]中给出了从给定的数据状态模型机构构造转换系统机构的方法。3应用变换系统的引入主要是为了规范和规范技术的形式化比较。例如，在[9]中，比较了进程演算CCS[16]和并行程序设计语言UNITY[3]中给出的交替位协议的规范。建立了它们的组件sender、channels和receiver（它们分别是CCS和UNITY中给定语义的保守扩展）的转换系统语义的发展关系，并讨论了它们的组成比较。这显示了公共语义域如何支持非常不同的规范的比较，根据它们的基本假设和规范范例（通过消息交换的握手通信与对共享变量的异步访问 在[11]其他规范方法的解释和整合如Petri网和图论的讨论。在[13]中，在变换系统的语义层次上引入的合成操作已被应用于图变换系统的新的合成操作。除了之前已经使用的图变换规则的合并之外，还支持如上所述的同步关系。它们指定哪些操作可以通过执行它们的合并规则来同步。这基于动作的（直观）同步产生了对系统组成的更多控制。转换系统的元素关系的另一个应用可以在[18]中找到，其中引入了类型化图转换系统的模块。这些由导出和导入接口以及使用导入接口所需的服务实现导出接口所提供的服务的主体提供。部件（出口、进口、7body）由任何方法中的类型化图变换系统规范给出。 出口与主体之间存在着一种关系，这种关系决定了出口服务是如何实现的。行为保护的相应概念|如一般变换系统所定义的|用于表明在导出接口处指定的预期行为由主体中的实现保证，并且相对于. r. t是稳定的。在[18]中定义的模块的组合操作。除了这些规范的形式主义，既有一个正式的语法和一个正式的语义，软件建模技术也被认为是。它们的语义通常只是非正式地定义的，就像统一建模语言的不同的图技术一样。软件模型和规范的集成再次通过它们在转换系统域中的共同解释来实现（参见[12]）。在这种情况下，它们可以用来提出建议，为正式的语义，这种建模技术，并在同一时间展示其相互关系和语义集成的可能性。4代数重写在前面的部分中，已经概述了转换系统的描述性框架。因此，还提到了变换规则作为系统变换行为的规范手段。这些变换规则也可以被构造性地解释，即，它们可以被应用于部分代数以变换它们，就像图语法规则被应用于变换图一样。其基本思想是简化代数|通过一个附加|到可以通过简单的集合操作（如减法、交集和并集）进行操作的表示。后者产生规则的预期效果：删除（减去）代数中规则左侧的图像，保留左侧和右侧相交的部分，并添加（通过并集）右侧的相应部分。（本节内容的更详细介绍见[10]。）设=（S; F）是一个代数签名。给出了一个表示P =（PS; PE），它是由一个S{索引集PS=（PS）s2S，生成元和一个集合PEEqns（PS），方程给出的. 如果PE是PS上的函数项的集合，则表示是函数的，即，PEff（a）= b jf：w！v2F; a2P w;b2 P v g方程式（P/S）：展示产生一个类别和与每个类别的部分代数PAlg（）的关系，其中=（; CE）是条件（存在）方程的扩展。一个偏{代数A由此被映射（通过右伴随t）到它的载体集合AS，并且它的函数e n尝试AE=ff（a）=bjfA（a）=bg。如果呈现P是功能性的和一致的，即，它不包含函数对e n尝试f（a）=b和f（a）=b0 如果b6=b0，则部分由P生成的代数本质上与P相同。否则元素8RRLRLRREEEX0 = Xl Xr Xc = Xl\ Xr X0 = Xr XlE0 = E1Er Ec = El\ Er E0 = Er ElBS：=（Asm（X0））]X0：S(i)首先，去除A的所有作为X0在m下的像的元素，（生成元）必须被识别和/或新元素必须被生成以满足条件方程。提出了一种变换规则r=（=^Pl！Pr）是由一个泛函{表 示 P1= （ X1;E1 ） ， 任 意 { 表 示 Pr= （ Xr; Er ） ， 以 及 动 作 表 达 式 = a（X1;：;Xn），其中形式参数X1;：;Xn是X1[Xr]的元素，并且a是具有适当参数类型列表的动作名称。令r的对称方向和交叉由下式给出：L rL r设A是一个具有表示PA=（AS; AE）的偏（; CE）{代数. A中r的匹配mt =（m; t）由表示态射m：P l给出！ PA，即，A中变量Xl的实例化，使得方程El的实例w.r.t.m被A满足，并且变量X0的绑定条款，即，一个映射t：X 0！ Term（X l[X r）. 然后重写步骤r=mt =（a（m（x 1）;：; m（x n））：A）B）将A重写为部分{代数B，其定义如下。X0的所有元素相加：L r(ii)从AE所有那些函数项是E0的实例， m是删除. 那么方程E0添加以及方程x = t（x）for x 2 X0的实例，表示根据匹配的t{部分将新生成的元素绑定到名称。b0的：=（AEE0[m]）[E0[m][f（x=t（x））[m]j x2X0 g：E L R R(iii) B0中的方程 可能仍然包含AS中存在的元素但他们已经不在BS 了。这些必须通过限制B0来解决 到BS：BE：=（B0）jB：(iv) 最后，结果B被定义为由{表示（BS; BE）自由生成的部分{代数：B：= PAlg（BS; BE）：请看下面的例子。创建规则c reat e（x）=^（;）！（x：s;;）可以用来创建一个新的元素，并将其绑定到一个标识符，例如由一个基础项给出。 让c：！ s是一个常数symbolin，A是一个部分代数，其中c是未定义的。然后通过以下方式911aJat（a）J23c4BDJ5del（3）z2T（B）S（C）C4s（d）dJ5图二. 删除具有活动约束的节点3。匹配m =1和t（x）= c产生由Bs=As]fxg给出代数B，其中x是不包含在As中的任意新元素nt，Bs0 =As0 对于所有s0 6=s，且BE=AE[fx=c g. 也就是说，x是c在B中的i的表示。 因此，在B中创建了一个新元素，可以通过名称C. 如果c已经在A中定义，那么B将同构于A，因为等式x = c和cA = c意味着x = cA。图可以被认为是由下式给出的特殊图的部分代数：各样 节点，边funs s，t：edge！节点ceqns s（e）#，t（e）#其中，r #是确定性谓词，对应于存在性方程r = r。这意味着，s和t必须是全函数。现在考虑以下删除节点的规则：del（n）=^（n：n o d e;;）！（;;;）例如，del（3）的应用如图2所示。在最后一步（BS; BE）7！由于规范中的一致性公理s（e）#; t（e）#（源和目标的总体），针对悬挂边重构重写源和目标的结果的构造的PAlg（BS;BE）= B。这意味着，公理成为主动约束，修复由删除引起的不一致。简单的图表，即，在两个节点之间最多有一条边的图，可以通过附B10加公理s（e）=s（e0）^t（e）=t（e0））e=e0来描述，或者通过下面的说明来描述，该说明将边引入为关系而不是具有自己标识的项。排序节点funs边：节点，节点11，，IlLLRLLEmt =（m; t）是无冲突的，即， X0和Xc的元素和E0的1 1J2 34del（3）z24J5 5图3.第三章。删除节点3，带边效应。在这种情况下，应用del（3）w.r.t.相同的规则产生图3所示的重写步骤。由于函数项对重写步骤中保留的元素的限制，与3相邻的边作为删除3的边被删除。（参见在页面上重写的构造的第三步骤8）。在一定条件下，重写可以用部分代数范畴中的交换图和推出来描述。这也产生了与图重写的DPO方法的正式比较（参见[4];与代数重写的其他方法的比较可以在[15]中找到）。让C是由表示（AS）生成的部分{代数 m（X0）;（AEE0 [m]）jC），表示重写步骤的删除部分。 如果匹配L l和Ec分别不被m标识，如图4所示其中Pc=（Xc;Ec），可以构造和交换。 (The态射i l：C！A和i r：C！B在图中总是存在，也产生重写步骤的跟踪关系：ab，如果存在c2 C，其中i l（c）= a和i r（c）= b。这个图特别显示了，如果匹配是无冲突的，则规则的右侧包含在结果B此外，如果不使用新变量（来自X0匹配mt的t{i}部分是包含，则图（2）是推出图。最后，如果m对X0的限制是单射的，并且没有边射，则图（1）也是推出图。（一个副作用是通过从A中删除一个函数项来给出的，它不是某个e2E的实例由于B0的限制 到B.）S关于具有代数重写规则的动力系统的特殊化，可以得出以下结论。具有条件存在方程的部分代数是一个强大的，系统状态表示的灵活手段。 数据和对象PAlg（P）PAlg（P）pr PAlg（P）L（1）C rc（2）rJ J JA CirB见图4。 重写步骤，，plS12例如，可以使用对象引用的堆栈。代数签名产生一种语言来表示不同状态的元素，这些状态可以产生它们的身份。(The在表示不同状态的不同代数中对符号性质的常数的求值产生其可变的、状态相关的值。然而，变换的识别关系可能更大。）新元素可以绑定到由签名的术语或常量给出的名称，这使得它们可以在子状态中访问。方程或其他公式可以用来明确地推理状态属性。代数的重写是非常普遍的（它可以应用于任意条件规范的代数），并且基于简单直观的集合运算。仅使用签名，代数的重写与元素和函数项的删除和添加W.r.t.代数重写规则的变换行为只是需要区分具有自己的恒等式和关系（没有恒等式）的项。两者都可以删除或添加，但在删除中，删除具有标识的项目具有删除该项目参与的所有关系的副作用。这些是唯一的侧面效应。规则没有匹配条件，除了必须满足显式陈述的方程的实例。5结论本文简要介绍了代数变换系统及其在比较和集成不同的形式和半形式规范技术中的应用。 在这个框架中，还可以比较图重写的不同方法，如第4节所讨论的。然而，对统一的主要贡献应该在转换系统框架所追求的一般语义方法中看到。这意味着，首先确定形式语义对象、操作和关系，然后寻找句法表示。这将变换系统方法与其他统一和比较特别是图形变换系统的方法区分开来。引用[1] L. Andrade，J. Fiadeiro，J. Gouveia，A. Lopes和M. Wermelinger协调模式。In G. Gruia-Catalin 和A. Porto ， 编辑， Proc. Coordination Languages andModels，Springer LNCS 1906，第317页{322，2000.[2] G. Booch，J. Rumbaugh，and I.雅各布森统一建模语言，用户指南。Addison-Wesley，1998年。[3] K.M. Chandy和J. Misra。并行程序设计基础.艾迪生-韦斯利，1988年.13[4] A. 科拉迪尼 Mo n tanari，F. Rossi，H. 埃里格河 He c kel和M. L哦，是的。图变换的代数方法I：基本概念和双推出方法。In G. Rozenberg，编辑，Handbook of Graph Grammars andComputing by Graph Transformation，第1卷：基础，第3章。World Scienti c，1997.[5] H. Ehrig，G. 恩格斯，J. J. Kreowski和G. 罗森伯格，编辑。 图形文法和图形变换计算手册，第2卷：应用程序、语言和工具。World Scienti c，1999.[6] J. Fiadeiro和T.麦鲍姆。作为并发系统规范的模块化单元的时态理论。Formal Aspects of Computing，4（3）：239{272，1992.[7] J. A. Goguen和R. M.伯斯托机构：规范和编程的抽象模型理论。ACM期刊，39（1）：95{146，1992年1月。[8] M. Gro e{Rhode. 代数变换系统及其组成。在大肠Astesiano，编辑，软件工程的基本方法（FASE'98），第107页。 Springer LNCS 1382，1998年。[9] M. Gro e{Rhode.基于代数变换系统的CCS和UNITY中交替位协议规范的合成比较。在K。Araki，A. Galloway ，and K.田口，编辑，Proc. of the 1stInternational Conference on Integrated Formal Methods（IFM'99），York，UK，28{29 June 1999，pages 253{272. Springer Verlag，1999年。[10] M. Gro e{Rhode.用代数重写系统和元素规范基于状态的系统。TechnicalReport 99{04，TU Berlin，FB Informatik，1999年3月。[11] M. Gro e{Rhode.基于转换系统的异构形式规格说明语义集成。 技术报告，柏林工业大学，2001年。[12] M. 格罗罗德 面向对象系统模型的集成语义。在J. van Leeuwen，editor，Proc. ICALP 2001，Springer LNCS，2001.[13] M.科赫图变换和时态逻辑在分布式系统空间划分中的集成。博士论文，Technisc heUniversitatBerlin，FB 13，1999.[14] H.- J. Kreowski和S.库斯克具有交错语义的图形变换单元。 Formal Aspectsof Computing，11：690{723，1999.[15] M.拉布尔斯代数的双推出变换。 PhD Thesis，Dept. de Ci encies Mathematiques i Informatica，Universitat de les Illes Balears，Palma de Mallorca，Spain，2001.[16] R.米尔纳 通信和并发。 普伦蒂斯·霍尔国际，1989年。[17] G. 罗森伯格编辑图文法与图变换计算手册World Scienti c，1997.14[18] M.西梅奥尼图变换系统模块化的范畴化方法。博士论文，Dip。di Scienzedell'Informazione，Universit a di Roma La Sapienza，2000.[19] 统 一 建 模 语 言 { 版 本 1.3 ， 2000 。 可 在 www.example.com 上 获 得http://www.omg。org/uml.[20] G. Winskel和M. 尼尔森 并发中的类别。 在A.M.皮茨和P. Dybjer，编辑，Semantics and Logics of Computation，Publications of theNewton Institute，pages 299{354. 剑桥大学出版社，1997年。
我的内容管理
展开
