UML组件的协同开发框架

理论计算机科学电子笔记122（2005）229-245www.elsevier.com/locate/entcs基于UML的协同开发语义框架孙梦a，1，Bernhard K.Aichernigb，Lu 'ıs S. Barbosac，2和张乃晓a，1aLMAM，北京大学数学科学学院，中国b联合国大学国际软件技术研究所c葡萄牙布拉加米尼奥大学信息学系摘要本文介绍了一个通用的语义框架，基于组件的开发，表示在统一建模语言UML。类，对象和状态图以及用例的共代数语义的原则，开发。本文还讨论了如何基于适当的行为细化概念，将开发过程中的细化步骤形式化。通过这种方式，研究了UML中基于组件的开发的正式基础，它允许从独立组件构建更复杂和更具体的系统保留字：统一建模语言，精化，UML，余代数1介绍基于敏捷的开发[22]作为一种新的有效范式被业界接受，并被广泛认为是未来几年软件工程的基石在基于组件的范例中，系统由组件的集合组成。每个组件都是一个组成1本研究得到国家自然科学基金部分资助60273001。[2]S.Lu 'ıs的作品根据POSI/ICHS/44304/2002号合同，在PURe项目范围内，Barbosa得到了FCT的支持1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.06.051230S. Meng等人理论计算机科学电子笔记122（2005）229有合同规定的接口。它可以独立部署，并由第三方组成。基于组件的开发是一个相当复杂的活动，这一点已经得到了广泛的认可，并且对于组件和组件组装的精确定义仍然没有达成普遍的共识。因此，基于组件的开发需要正式的基础，特别是在广泛使用的面向组件的设计符号，如UML [20]。这里报告的研究的出发点是观察到，共代数结构[11，21]不仅可以为组件提供强大的语义域，而且还可以为定义和推理系统行为提供方便的技术因此，本文的目标是建立一个语义框架，在这个框架中可以映射UML中最流行的符号，以便为严格的基于组件的开发提供基础。本文首先简要介绍作者在以前的一系列论文[1，2，3]中提出的在第3节中，我们将对UML中使用的一些关键图进行共代数表征。在第4节中，作者以前在[ 15 ]中讨论的关于共代数模型的精化的工作，被框架化为需要适当的UML模型精化的这不仅使（部分）UML描述的形式化，而且使其转换成为逐步单独开发的基础。最后，在第5节中讨论了未来工作的前景。2作为余代数在这一节中，我们介绍了一个基于状态的组件的余代数模型，紧Bar-bosa等人在[1，2，3]中。这种方法提供了一个观察语义的软件组件和一个通用的组装演算，在这个意义上说，建议的结构是参数的组件行为的概念。组件通过接口与环境交互每个接口都提供了一组类型化的通道，用于接收和发送消息，充当相应组件的类型。定义2.1设I和O分别是输入和输出通道的类型集合。对（I，O），用I→O表示，称为接口，任何具有这样一个接口的组件p都被类型化为p：I→O。在最简单的确定性情况下，组件p的行为是上限-S. Meng等人理论计算机科学电子笔记122（2005）229231×→P我∈→×O）P由它所产生的输出来决定，而输出是由所提供的输入来决定的。但现实往往更为复杂，因为人们可能不得不处理其行为模式的组件，例如。、部分或甚至非确定性。因此，为了以通用的方式进行，行为模型被抽象为强单子B。当然，B=Id检索简单的确定性行为，而B=或B=Id+1将分别对非确定性行为或部分行为进行建模。 因此，一个分量p：I O可以用集合内函子TB=B（IdO）I的余代数来建模。这样，它的计算将不会简单地产生输出和延续状态，而是产生这样的对的B-结构。形式上，这样的分量p被建模为一个指向的具体余代数<$Up，αp：Up→B（Up×O），u0∈Up<$其中，特定值u0被视为其连续观察一个分量p，揭示其允许的行为模式。 对于每个状态值u Up，p在u处（更准确地说，从u开始）的行为将其自身组织成一个树状结构，因为它取决于所处理的输入项的序列。 这样的树，其弧标记为I值和节点标记为O值，可以用从非空序列的I到B-输出项结构的函数来表示。换句话说，空间具有接口I的组件的行为的集合是（BO）I+，它在事实上，最终 TB-余代数（νT，ωT：νTTBνT）的载体νT 因此，通过finality，从任何其他TB-余代数p，有一个唯一的态射[（p）]使下面的图可交换：νTˆ（p）UpωT）B（ναp）B（U我ˆB（[（p）]×O）I×O）将态射[（p）]应用于状态值u∈Up给出了从u开始的p个转移序列的可观察行为。通过用具体的强单子（如和Id+1）实例化B，可以分别对不同的行为模式（如非确定性和部分行为）建模。在将一般成分定义为具体的余代数之后，人们可能会自然地想知道它们是如何组合的，以及从这个框架中出现了什么样的演算。组件是不p我232S. Meng等人理论计算机科学电子笔记122（2005）229⟨⟩×pτr范畴框架来构建我们的语义世界。简单地说，我们构造了一个以界面论域I，O，···为对象，以具体余代数为种子，以2-胞腔（箭头之间的箭头）为对应的余代数态射的双胞腔Cp2-cell组合继承自Set分量p上的单位元定义为p的载波上的单位元idUp。然后，对于每一对对象I，O，Cp的构造定义了一个hom-categoryCp（I，O），其箭头h：<$Up，αp：Up→B（Up×O）I，up∈ Up <$$>→ <$Uq，αq：Uq→B（Uq×O）I，uq∈Uq<$是满足以下条件的映射h：Up→Uq：α q·h=T Bh·α p， hu p= u q对于每一个三元组的对象<$I，K，O<$，一个复合律由一个函子给出：;I，K，O：Cp（I，K）×Cp（K，O）→Cp（I，O）其对分量p和q的作用由下式给出：p;q=<$Up×Uq，αp;q，<$up，uq<$∈Up×Uq<$其中，αp;q：Up×Uq×I→B（Up×Uq×O）详细描述如下3：αp;q ：Up×Uq×I−−=−→U×I×Uqαid−−−→ B（Up×K）×Uq−→B（UpB（id×αq）×K×Uq）−−=−→B（UBτl×（Uq×K））−→B（Up×B（Uq×O））−→BB（Up×（Uq×O））−−=−→BB（U×U×O）−µ→B（U×U×O）q−−p q“;”在2-胞腔上的作用简单地由h ; k = h × k给出。最后，对于每个对象K，由函子副本K：1 → Cp（K，K）给出一个恒等律，它对对象的作用是常数分量<$1，αcopyK，<$∈ 1 <$，其中αcopyK=η1×K 。类似地，同态的作用也是常态射id1.除了上面定义的“流水线”顺序组合，组件可以以多种不同的方式聚合。在[2]中，从Cp的结构中出现了一个演算，包括一个最后，广义的相互作用是通过一种3噪声是最大的和最大的，η是单位的和τr的，τl是左强度的。pppS. Meng等人理论计算机科学电子笔记122（2005）229233→3UML的形式化语义我们对UML形式化研究的中心思想是一组UML图表示由Jacobs [8，9]引入的共代数规范。更准确地说，我们打算将UML语法中的所有图形符号和注释转换为一个共代数规范的函子和属性。因此，泛余代数中的标准定义，如双相似性和精化，可以用来推理和转换UML设计。3.1类图UML描述中的一个主要组成部分（如[17]所示）是类图。类图显示了系统的静态结构，由一组类和它们之间的关系在UML中，类是对一组具有相似结构、行为和关系的对象的抽象描述。一个类的描述包括属于它的所有对象共有的属性和操作。系统中C类的每个对象o都有一个标识符ido，它在系统中是唯一我们用Id表示所有标识符的集合。因此，对象o：C表示为三元组o=（ido，UC，αC：UCT（UC）），其中UC是状态C类空间，由C对象的所有可能状态组成，T是封装属性和方法签名的仿函数。在对象的生命周期内，其局部状态可能会改变静态空间UC，但它确定UC本身和转换结构αC保持不变。在Jacobs等人[7，8，19]关于共代数语义的工作之后，UML类图中的每个类都被视为一个共代数规范Spec，即。、定义3.1一个共代数规范Spec是一个元组（T，Φ， Ψ），其中：• T是局部状态空间U上的函子，表示类的所有属性和方法的签名;• Φ是一组公理，给出了对属性和方法的函子的约束，以表征类的属性• 是描述新创建对象的属性的公理。给定类规范Spec=（T，Φ， T）的模型（类实现）是三元组c=（U，α：U→T（U），u0），其中U是解释类的状态空间的载体集，α：U→T（U）是满足Φ给出的所有性质的过渡结构，u0∈U是满足Φ的初始状态。定义了UML类图中具体类C的语义234S. Meng等人理论计算机科学电子笔记122（2005）229C cCC在CPPCC00作为范畴Coalg（Spec），其对象是对应的余代数类规范Spec的模型，箭头是它们之间的保持初始状态从形式上讲，[[C]] =Coalg（T，Φ，θ）ifisAbstract（C）=Falsewheree（TC，ΦC，CXC）是类C的具体化，而布尔值函数is Abstract则指定类C是否可以直接实例化。这个范畴是Cp的一个子范畴，在上一节中定义。具体来说，其对象Obj（Co alg（TC，ΦC，αC））={c=（UC，αC：UC→TC（UC），u0∈UC）|（c）在|= Φ C）（c，u0|= C）}其中c| = Φ C意味着Φ C中的所有公理都被余代数c和c满足，u0|= C意味着C中的性质由c的初始状态u0满足。它们的正式化对本报告的目的来说是无关紧要的。本文现在让我们来看看属性的具体化默认的UML语法是可见性名称：type-expr[多重性排序]=初始值{property-string}因此，C类中属性At的语义功能定义如下：[[v At：T[m] =i{p}]]={At：U→T（U）|[[At[m][[At=i]][[At{p}]]}其中，T=[[T]]，与代表幂集函子，需要它来建模属性类C中属性At的多重性的语义是[[At[m]=0或者，如果指定为范围，在...在... k]=U∈UC. card（At（u））=mU∈UC. l≤card（At（u））≤k初始值用于初始化新创建的对象的属性。因此，我们认为，[[At=i]]=Δt（U， α， u）∈Obj（[[C]]）.At（u）=i可选的属性字符串指示属性的属性值，如可变性。由于长度限制，我们省略了它的语义以及S. Meng等人理论计算机科学电子笔记122（2005）229235∈联系我们学生*接受课程*当然name：String学生ID：编号name：StringcourseID：Number学生课程Fig. 1. 协会用于属性、操作、接口等的可见性的语义功能这是可以在[14]中找到的请注意，在这个框架中，属性和操作非常相似：只有签名函子的形式发生了变化。区别在于观察和计算之间的区别，只有后者才是对象状态变化的来源类图中的关联描述了系统中对象之间的连接它可以具有两个或更多个缔合末端。图1显示了一个关联的示例。假设SpecU和SpecV是类图中类U和V的类规范，A是它们之间的二元关 联。 还 假 设c= （ U ， α ， u0 ） 和 d= （ V ， β ， v0 ） 分 别是 Coalg（SpecU）和Coalg（SpecV）中的对象。那么连接两个余代数的结合A可以被解释为空间SA（（Id U）（Id V））。集合Id中的标识符是区分处于相同状态的同一类的对象所必需的。元素SA是关联的状态，其记录由关联同时链接的一组对象对在s处配对的各个状态。SA中的每对对象称为它们之间的链接。每一个关联都有三个基本组成部分：一个名称、一个角色和其两端的多样性。 关联的语义由关联所关联的每个类中相应的观察者给出。设A是类U和类V之间的这样一个关联。两端的角色名和多重数分别是uA，vA和mU，mV，后者是两组非负整数。然后A的语义被定义为一对共代数观察者：（uA：（Id×V）→ P（Id×U），vA：（Id×U）→ P（Id×V））（1）其中U和V是对应于类U和V的语义的余代数（U，α：U→TU（U），u0）和（V，β：V→TV（V），v0）的状态空间。此外，两个共代数观测器必须如下相关：oU∈uA（oV）惠oV∈vA（oU）（2）严格地说，由结合A连接的是它们的类：而两个余代数由A的一个链连接。236S. Meng等人理论计算机科学电子笔记122（2005）229一mUA mVvAmUAC mV一UV一1MV微米的1综上所述，关联的语义由（1）中的观察者对给出，其满足（2）：[[UuAvAV]]={（u，v A）|（二）UML规范[17]指出，每个关联端都有一个多重性约束（在不完整的模型中可能是未指定的），它是如果在图中明确给出多重性，则语义函数将变为：[[UuAvAV]]={（u，v A）|（2）（o U：Id × U。（卡（vA（oU））∈mV））（第五节：Id × V。（card（uA（oV））∈mU））}UML提供了一整套可选属性，可以在类图中赋予关联例如，UML允许一个关联拥有自己的属性，这些属性由一个关联类表示，即一个关联，它也是一个类。通常，关联类可以表示为具有两个一对多关联的类。因此，一个关联类的语义是通过这个类的语义与两个关联的语义的元组来定义的，如下所示：[[UuVvUV]]=<${（ac，（u， a），（a， v））|ac∈Obj（[[AC]]）<$（uA，aU）∈[[UuA−aUAC]]<$（aV，vA）∈[[ACaV−V]]<$U：Id × U，V：Id × V。（（oV∈vU（oU）惠快！oA：Id×AC.oV=vA（oA）oA=aU（oU））（oU∈uV（oV）优惠券！oA：Id×AC.oU=uA（oA）oA=aV（oV）}最后一个谓词通过AC在两个方向上确保对象链接的良构性。现在让我们转向泛化的语义学。类图中的泛化描述了一般类（超类）和更特殊的类（子类）之间的继承关系。在类图中，类D是C的子类的事实表示为CD−−D。 这是一个很好的例子，D继承了C。如果D和C之间存在这样的继承关系，则可以导出相应模型范畴之间的遗忘函子G：Coalg（D）→Coalg（C），如[7]所示。在我们的框架中，UML类图中的泛化关系的语义是通过收集模型之间所有可能的继承态射来给出的，一一S. Meng等人理论计算机科学电子笔记122（2005）229237∆1→212n相应的类规范，即、[[CD−−D]]=<${g：d→c|d∈Co alg（D）<$c∈Co alg（C）}其中g是从d到c的继承态射。 这种态射由一个遗忘函子和对应于两个类的函子之间的自然变换构成。泛化关系将类组织成一个格，最泛化的类位于层次结构的顶部（最终成为一个抽象类）。meet和join运算符分别被定义为类的超类和子类（用于多重继承）。注意，抽象类可能没有直接实例，因此，它不能以与具体类相同的方式解释然而，从抽象类和它的子类之间的泛化关系，它的语义可以恢复为它的所有子类的最小超类（或类格中的最小上界）。转换为范畴论，这意味着抽象类关于其子类的语义是对应的子类余代数的余极限，即。、[[C{Abstract}D−{C，C， . . 得双曲余切值.}]] =Colimit（c，c，.（c）其中ci分别是[Ci]中的余代数。3.2对象图和类图我们现在可以总结前面的讨论，集中在类级别，以给出类图的语义，它是通过对象图定义的。对象图是相应类图的快照。它展示了系统中特定时间点的一组对象及其关系这些对象及其关系在语义上定义如上。因此，用Σ表示系统状态空间，一个对象图表示一个系统状态σ∈Σ，并且可以被看作是相应的类图的一个实例。因此，元素σ∈Σ可以解释为不同对象在同一时间点的然后，系统可以被建模为一个余代数c=（α，α：α→T（α）），其中α描述了系统状态之间所有可能的转换从形式上讲，定义3.2类图CD的语义由范畴Coalg（CD）定义，其对象是余代数（coalgebras，c：coalgebras）。T（k）），其中k是包含所有可能的系统状态的系统状态空间。 T是组件类的所有签名函子的张量积nCP238S. Meng等人理论计算机科学电子笔记122（2005）229→和关联，描述可能的系统状态转换和观察。箭头是它们之间的T-同态3.3用例在UML中，用例描述功能需求。用例被定义为 因此，我们可以用共代数的方法将用例解释为一系列动作，后面跟着一些（最终组合的）观察结果。单个操作表示将系统从一种状态更改为另一种状态的原子用例。 这样的动作包括创建新对象和删除旧对象，形成或删除对象之间的链接或修改对象的属性值。原子用例的签名再次由函子T定义。假设系统状态空间是系统状态空间，如类图的语义中所定义的。然后一个用例被解释为一个函数uc：WNT（WNT）。一个例子应该演示用例的共归纳形式化。考虑一个描述在图书馆借书的过程的用例BB（完整示例见[14]），如图2所示。设k为系统的状态空间。那么BB的行为可以用一个共代数函数bb：→Student×Book来定义。如果学生s0借了书b0，那么可观察的效应可以共归纳地指定：前贷款（sJ0（bb（σ，s0，b0）=贷款（sJ0（σ））<${b0}前向借款人（BJ0（bb（σ，s0，b0）=SJ0（σ）其中SJ0，BJ0是用于获得对象s0，b0和σ∈Σ的Σ上的观测器。注意，前提条件pre的目的是保证类图中的多重约束。除了系统操作之外，行动者还可以执行其他动作来改变系统状态。因此，通过将系统操作和参与者操作集成在一起，用例可以更通用地如何在我们的框架中具体说明这一点？第2节中提到的组件演算提供了一组组合子（特别是顺序和并行组合），可以用于从组合原子用例中获得更复杂的用例例如，用例BB被定义为对应于事件1和2的原子动作的顺序组合，当条件为真时，返回一本书的另一个用例对应于事件3，以及事件4。S. Meng等人理论计算机科学电子笔记122（2005）229239→用例借书行为者读者，图书管理员前提这本书可以借。事件流1. 当读者选择一本还没有借出的书时，用例就开始了;2. 图书管理员检查读者是否还能借更多的书;3.如果读者借的书的数量达到了上限，包括退货单;4. 图书管理员指定读者为图书的借阅者，并规定一个截止日期把书还回来后置条件读者成功地借到了这本书。图二. 借阅图书用例3.4状态图在UML中，状态图描述了系统的动态行为。以前已经提出了几种状态图的形式语义。例如，在[13]中，输入-输出标记转换系统被用作语义域。我们的目标是给出统计图的一个余代数特征，这样，类图和状态图之间的一致性检验就变成了余代数（状态图）是相应的余代数规范（类图）的一个模型的证明。类似地，细化（实现）关系可以在不同的视图模型上定义由于状态图的层次结构，我们将赋予配置集由操作语义诱导的共代数结构，而不是简单地在状态集上构造共代数结构。函子T捕捉了这样一个余代数的形状：T（X）=B（X× PE）E其中E表示所有事件的集合-注意，在此阶段，事件可以具有参数而不仅仅是原始信号。B是一个强单子，它指定了状态图的行为模式（通常是幂集单子）。对于给定的状态图SC，设CF为配置集，（CF，α：CFT（CF））为对应的T-余代数.因此，SC的行为由下式给出：[[SC]]：λs：CF。 α（s）请注意，直接定义共代数语义可能会导致更忠实的模型，因为我们可以自由地选择签名函子。关于验证，当与直接编码作为Kripke240S. Meng等人理论计算机科学电子笔记122（2005）229结构，并使系统性能的验证更有效（如D. Pattinson in [18]）。详细讨论见[16]。此外，作者在[15]中提出的组件细化的一般概念可以适应UML的上下文，并用于检查不同模型的一致性。这就是下一节的目的。4细化为了在开发过程中正确使用UML模型，我们需要一个清晰的组件之间的细化概念，澄清一个组件实现另一个组件意味着什么。垂直于系统结构的水平分解，从抽象组件中提取具体组件的垂直细化在本文所勾画的余代数框架中，可以定义三种成分之间的精化关系。在任何情况下，为UML模型定义的语义映射使它们与适当的细化排序相关联。• 行为细化，通常将相同接口的组件关联起来，其中细化基于两个由于同一接口的组件之间的态射实际上是余代数同态，因此，需要双相似性，我们必须寻求一个较弱的概念，组件之间的态射，仍然保持源组件的动态。关于UML，这种细化主要用于行为模型的细化，特别是状态图。• 接口改进，这与人们可能称之为插接兼容性有关。它涉及不同接口的组件，问题是一个组件是否可以通过适当的布线进行转换，以替换另一个具有不同接口的组件。由于组件接口类型的结构编码了可用的操作，这可以捕获组件功能扩展的情况，在这个意义上，“具体”组件可以引入新的类图和用例。• 和架构细化，用于将具有指定行为的组件分解为分布式系统架构，即，一个家庭的组成部分，并行组合，这也是作为一个具体的余代数建模。这种细化的概念主要用于系统架构的开发，即，查看组件和部署图。S. Meng等人理论计算机科学电子笔记122（2005）229241胡适⟩⟨ ⟩≤·≤·我们说一个分量p在行为上修饰了分量q，如果观察到的p的行为模式是q的行为模式的一个结构限制，相对于单子B所捕获的行为模型。为了使这样一个因此，将分量p视为q的行为细化的一种可能（且直观）的方式是认为p个跃迁在q中保持不变。对于非确定性组件，这被简单地理解为集合包含。 但也可以考虑其他限制。例如，为了规定如果p没有从给定状态的转换，则q也应该没有从对应状态的转换。回想一下，从p到q的分量同态是一个种子保持函数h：Up−→Uq，使得B（h×id）·αp=αq·（h×id）。就转换而言，该等式被转换为以下两个要求（通过[21]中的论点的直接概括）：乌吉岛−→pu我，O−→qv⇒hu−→qhu我，O⇒uJ∈Us. t. u −→ pu吉乌河 =hvJ（三）（四）其捕获了这样的事实，即不仅由引入的转换关系表示的P动态被H（3）保持，而且Q动态也在相同的H（4）上被反射为了定义一个较弱的余代数态射的概念，设是集合内函子T[10]上的一个序（具体地说，将每个集合U映射到一个≤TU的前序集合），称为加细前序。然后，定义4.1设T是集合上的扩张多项式函子，考虑两个T-余代数p=（U，α：U→T（U））和q=（V，β：V→T（V））。关于一个加细预序≤的前向态射h：p→q是从U到V的函数，使得Th·α≤β·h连接两个分量p和q的前向态射的存在证明了一种精化情形，其对称闭包与互模拟相一致。在续集中，我们将行为细化定义为前向态射的存在性直到互模拟5。从形式上讲，定义4.2给定分量p和q，p是q的行为精化，[5]在[15]中，一个向后态射的对偶概念，即，，一个满足βhThα，也进行了研究，导致了一个概念的向后微调，这确实有一些应用，虽然潜在的直觉似乎不太熟悉。JJ242S. Meng等人理论计算机科学电子笔记122（2005）229± ∼∼±⟨⟩±关于我们写为pB q，如果存在分量r和s使得p r，q s，并且存在从r到s的（种子保持）前向态射。行为细化的特点是保持组件的特性。但是如果我们仅仅依赖于行为细化，那么无法改变语法接口将迫使我们在整个开发过程中为了避免这种情况，引入了一个更通用的精化概念，称为接口精化，它将组件与不同的接口联系起来。定义4.3设p：I→O和q：IJ→OJ是分量。如果存在函数w1：IJ→I和w2：O→OJ，使得p[w1，w2]±Bq则p是q模向下函数w1和向上函数w2的接口加细，记为p±（w1，w2）q。接口改进支持从现有组件系统地构建新组件。一般来说，对于任意分量p和函数w1，w2，p±（w1，w 2）p[w1，w2]这种技术很有用的一种情况是，当我们有一个已经完成的现成组件，并希望调整该组件的语法接口因此，接口精化为组件的接口适配提供了一个系统化的模式上面介绍的两种细化关系都是根据组件的底层黑盒行为定义的。然而，当我们开发一个系统时，仅仅描述它的黑箱行为肯定是不够的，我们还需要捕捉一些内部结构方面。为此，我们引入了建筑细化的概念。为此，让我们将体系结构定义为元组S=I，O，C，R，其中I和O分别是系统的输入和输出接口，C=pk=Uk，αk，uk kk=1，2，···，n表示有限的分量集，R表示有限的组合子集以及由它们组合的分量。事实上，系统可以被分层分解，并再次被视为普通组件，这意味着行为细化的概念仍然适用。因此，架构细化关系被定义为给定接口内的行为细化：定义4.4设S和SJ是两个系统。如果I = IJ，O = OJ，且[S]] B[[SJ]]，则我们说S是S j的结构精化，记作SA SJ。S. Meng等人理论计算机科学电子笔记122（2005）229243细化概念最明显的用途是比较同一组件的两种替代设计我们将每个设计作为UML中的一个单独的模型，并通过将它们的语义定义为余代数来在语义级别上比较它们。对于M1和M2UML模型，我们定义M1±BM2惠[[M1]]±B[[M2]]M1±（w1，w2）M2惠[[M1]]±（w1，w2）[[M2]]M1±AM2惠[[M1]] ±A[[M2]]细化顺序的另一个用途是检查同一系统的模型之间的一致性。5结论和今后的工作我们已经提出了一个通用的语义框架，用于基于组件的开发，从UML描述开始，扩展了以前在组件软件上的工作，这些工作在一系列论文中详细描述，这些论文的口号是本文提出了UML类图的共代数语义的基本部分。它已经详细展示了UML图中的类、关联和泛化如何被解释为共代数规范。 此外，还对对象图、用例图和状态图的形式化进行了展望。虽然，空间限制排除了对其他图的更技术性的讨论，但读者现在应该知道共代数语义如何促进UML的静态和动态方面我们框架的另一个主要方面是细化，将组件的可替换性形式化细化是顺序编程中一个非常基本的思想然而，对于基于组件的系统，情况要复杂得多（参见，例如，[4]）。在本文中，我们在三个相互关联的层面上研究了我们的框架允许细化的概念来改变组件的接口和粒度。我们工作中的一个主要成就是Jacobs和Tews对面向对象系统的研究[8，9，23]。然而，我们并没有定义和求助于一种特殊（共代数）规范语言（CCSL），而是采用了一种相当实用的方法：使用UML图来表示共代数规范。我们的工作与[23]中UML的形式化之间的另一个不同之处在于，我们不将自己限制在类图中。244S. Meng等人理论计算机科学电子笔记122（2005）229实际上，本文打算是一个统一的UML的共代数语义的一步。目前，我们的研究计划包括进一步的工作用例，状态图，和合适的概念之间的一致性UML模型。进一步的UML元素，如交互图，将在后面的阶段讨论。在框架中提供的演算是一个promising- ing候选模型的相互作用。然而，仅仅有一个正式的语义是不够的。下一步将涉及语义的应用研究：我们的长期研究目标是提出一个用例驱动的UML设计开发方法，由代数定律和共归纳证明方法支持。在技术方面，该方法将得到一个模型检查器和一个UML图测试案例生成器的支持。引用[1] 我是S. Barbosa.这是一个基于数据库的计算工具。UniversalComputerScience，9（8）：891-909，2003年8月[2] 我 是 S.Barbosa and dJos`eNunoFon secadeOliveir a.STATT E-B ASEDCO M PONENTSMADGEN ER IC. In H.彼得·古姆，《选举》杂志编辑。笔记在Theor比较科学(CMCS'03 -计算机科学中的共代数方法研讨会），第82.1卷，华沙，2003年4月。[3] 我是S. Barbos和Sun Me n g。一般性犯罪。InGrahamHuttonn，editor，Proceedingsof FirstAPPSEM-II Workshop，Nottingham，March 2003.APPSEM Network Report.[4] Manfred Broy和Ketil Stølen。Specification and development of interactive systems：focuson streams，interfaces，and refinement，计算机科学专著第62卷。Springer，2001年。[5] 威廉-保罗·德·罗弗和凯·恩格尔哈特。数据精炼：面向模型的证明方法及其比较。剑桥大学出版社，1998年。[6] 查尔斯·安东尼·理查德·霍尔数据表示的正确性证明。Acta Information，1：271[7] 巴特·雅各布斯。继承和cofree结构。P. Cointe，编辑，欧洲面向对象编程，LNCS第1098卷，第210施普林格，柏林，1996年。[8] 巴特·雅各布斯。对象和类，共代数。 芽孢杆菌中 弗赖塔格角 Lengauer C.B. 琼斯和H.- J.Schek，编辑，Object-Orientation with Objectelism and Persistence，第83-103页。Kluwer，1996年。[9] 巴特·雅各布斯。在coalgebraic specification练习。In R.巴克豪斯河Crole和J. Gibbons，编辑，Algebrahem and Coalgebrahic Methods in the Mathematics of Program Construction ，LNCS第2297卷，第237-280页。施普林格，2002年。[10] 巴特·雅各布斯和杰西·休斯。余代数中的模拟。In H.彼得·古姆，《选举》杂志编辑。 笔记在Theor比较科学(CMCS'03 -计算机科学中的共代数方法研讨会），第82卷，第245-263页，华沙，2003年4月。[11] 巴特· 雅各布斯和简· 鲁滕。关于（余）代数和（余）归纳法的教程。 Bulletin of theEuropean Association for Theoretical Computer Science，62：222-259，1997.[12] 伊瓦尔·雅各布森工业环境中的面向对象开发。在诺曼K。Meyrowitz，编辑，面向对象编程系统、语言和应用会议（OOPSLAS. Meng等人理论计算机科学电子笔记122（2005）229245[13] Diego Latella，Istvan Majzik，and Mieke Massink. UML状态图的形式化操作语义。1999年FMOODS会议Kluwer，1999年。[14] 孙梦和伯恩哈德·艾希里希。面向UML的共代数语义：类图和用例。技术报告272，联合国大学/软件技术研究所，2003年1月。[15] 孙明和刘氏。 Barbosa。关于广义S-基S的W-分量的再定义第10届国际代数方法与软件技术会议论文集，AMASTSpringer，2004.[16] 孙明，张华纳，和卢伟思。 Barbosa. 关于S的代数和R的定义：一个共代数观点第二届IEEE软件工程与形式方法国际会议论文集。IEEE Computer Society Press，2004.[17] OMG. OMG统一建模语言规范，版本1.4，2001。[18] 德 克 · 帕 丁 森 。 Coalgebraictechniquesinmodelchecking ， 2001 。 可 查 阅http://siskin.pst.informatik.uni-muenchen.de/pattinso/Publications/。[19] 霍斯特·赖歇尔基于终结余代数的对象语义研究。计算机科学中的数学结构，5：129[20] 詹姆斯·兰博伊瓦·雅各布森和格雷迪·布奇统一建模语言参考手册。艾迪森·韦斯利·朗曼1999年[21] 扬·鲁滕泛余代数：系统理论理论计算机科学，249：3[22] 克莱门斯·西佩斯基组件软件-艾迪生-韦斯利，1998年.[23] 亨德里克·特斯面向对象规范的共代数方法。博士论文，德累斯顿工业大学，2002年。