UML模型与形式模型双向转换的研究

摘要

UML提供了图形概念来表示面向对象软件系统的设计。在软件设计领域，它已经成为了事实上的工业标准。然而UML缺乏精确语义且是一种半形式化语言。形式化规格语言试图为软件开发提供一种精确的、完备规格说明方法。许多研究者做了许多研究工作来把UML模型转换到形式模型以分析和验证UML模型。但是由于很难证明形式描述和非形式描述之间的等价性，因此需要在两个领域之间进行不断的来回往复。因此需要形式模型逆向转换回到UML模型。
　　 Z语言易于描述软件系统的静态结构，因此本文首先利用UMLTranZ的方法实现了UML模型到形式模型的转换。UMLTranZ方法能够将UML概念类图转换到Z模型。Z模型的主要架构是Schema，它能够形式的描述UML概念类图的语义。利用现存的形式模型分析工具可以对Z模型进行分析推理和证明。
　　 XMI(XML Metamodel Interchange)是由OMG提供的模型交换数据格式。利用XMI提供的传送模型不同部分的机制，我们提出了一种形式模型逆向转换UML模型的转换方法。这种逆向转换方法是一种间接的逆向转换方法，它能够在最大程度上减少UML模型转换到形式模型过程中所产生的弱化影响。将这种逆向转换方法与现有正向的转换方法向结合就能成功的实现UML模型和形式模型之间的双向转换。
　　 我们还利用了UTP理论形式的证明了逆向转转换方法的正确性和可行性。对应于通过UMLTranZ所得到的Z模型，我们基于一阶逻辑谓词和集合论定义了Z模型到UML概念类图的逆向转换具体映射规则。利用所定义的映射规则，可以间接的实现Z模型到UML概念类图的逆向转换。将这种逆向转换技术和UMLTranZ结合在一起，我们就能实现UML和Z之间的双向转换。
　　 最后我们设计了一个模型双向转换工具，并利用Java语言开发了一个原型。