UML/OCL模型的改写语义研究和工具开发

UML是一种国际标准的面向对象建模语言，但它缺乏一个完全的、精确的形式语义，导致它的一些概念和定义模糊，防碍了对UML模型的正确理解、实现和验证。本项目以改写逻辑作为语义框架，研究UML/OCL动态模型的操作语义。探索将UML/OCL静态和动态模型翻译成Maude语言的函数和系统模块的方法，探索将OCL表达式翻译成在Maude模块扩展上的项的方法，建立翻译工具。以Maude改写机为基础，开发状态改写机以实现我们定义的操作语义，开发OCL表达式评价器；在 Maude上模拟执行软件系统，证实其特性。这样的形式化技术能够帮助软件系统的分析和设计，在实现之前就很好地理解其结构和行为，提高软件质量。研究成果将促进我国在UML/OCL形式化领域的进一步研究，缩短我国与欧美国家的差距。本项目将培养3-4名研究生，在国内外核心期刊上发表4-5篇论文。

项目的背景：UML在软件工业已获得广泛的应用。人们对UML的研发集中于建模应用和工具开发，如UML作图、从UML模型产生代码、从源码提取UML模型。OCL描述UML模型的细节。由于OCL是形式化语言，建模者不易理解，难于写出OCL表达式。UML工具基本上不支持OCL，只有几个专门的OCL工具。UML标准以元模型定义，没有基于严格数学和逻辑的形式语义。十多年来，研究者探索UML的形式语义和验证方法，有两个途径：采用成熟的各种形式化方法，使用它们的工具；开发新的形式化方法，但这个方向的工作不多。大多数工作把UML和OCL分开来研究，因为两者都是庞大的。在我国，程序员会做软件系统的UML建模，学术界集中开发UML工具，但对UML和OCL的理论基础的研究较少。我们研究UML/OCL模型的理论基础且开发支持工具。主要研究内容：1）研究UML/OCL类图的代数描述，把类图翻译成Maude的函数模块，制定翻译规则。2）以改写逻辑（RL）分别定义UML状态图、活动图、顺序图、通信图的操作语义，给出推导规则。3）统一这些UML图的RL语义和推导规则。4）在Maude上，开发状态改写机，实现我们定义的RL语义。5）开发OCL表达式评价器。重要结果：1）我们研究了UML状态图的RL语义，定义了一组规则，目前仍在改进推导方法。2）我们探索了OCL的应用，以图书馆流通管理系统的UML/OCL建模为例，设计了大量的OCL表达式。我们正开发OCL导航的一个集合论语义。3）我们研究了面向对象语言的行为子类型，定义了一种简单的代数语义。我们计划研究UML和OCL中的行为子类型语义。4）我们开发了一个UML工具原型，支持UML建模，画出类图，从源码提取类图。我们正尝试开发UML模型到Maude模块的翻译器。科学意义：我们研究UML/OCL模型的形式语义指导工具的开发，帮助理解和使用模型；我们设计模型的OCL表达式促进OCL的理解和应用；我们开发工具用于建模和验证模型。