论文摘要
模型驱动开发（Model-Driven Development,MDD）已成为软件工程技术的研究热点和发展趋势,它通过提升抽象层次来应对软件开发的复杂性。模型转换是MDD方法中的一项关键技术,模型间的映射关系是模型转换的基础和依据。但目前关于模型转换的研究成果大都集中在模型操作的描述方面,其目的是实现转换过程的自动执行,而在映射关系的定义原则,以及转换规则的可行性和正确性验证等方面,还缺乏坚实的理论基础,从而导致了MDD研究的理论和实现不完善,模型转换难以满足实际需要的现状。模型转换的正确性问题是所有基于模型驱动的软件工程实施的基础问题,也是模型驱动开发研究的核心问题。模型转换正确性的一般标准包括语法正确性、语法完备性、可终止性、合流性和语义一致性。在这几个转换标准的判定上,除语义一致性外,其它几个语法层次上的正确性问题都已有相对成熟的解决方案。而在模型转换的语义一致性验证和分析方面,目前还没有成熟的理论基础和验证工具,模型转换中语义特性保持的定义、描述和验证仍是一个尚未解决的难题。如何保证模型转换前后的语义一致性,是模型驱动方法走向实现的关键。但在目前的MDD实现方法中,形式化语义的缺乏使得高层模型的描述还不够完备、精确,难以有效的支持模型转换和代码生成,也不能建立有效的评价和验证机制。缺乏模型转换相关的语义特性描述和计算,是当前基于MDD的软件开发研究中所缺乏的主要理论。建立模型转换相关的语义描述和计算理论是促进MDD方法健康快速发展的基础和当务之急。国内外多年的实践和市场的验证表明,软件体系结构和MDD的结合在软件的快速开发、随需应变、质量保证以及成本控制等方面是成功的,有很好的发展前景。基于以上的应用背景和需求,本文立足于解决模型转换的基础理论和技术问题,吸收软件体系结构和软件形式化等方面的研究成果,在对模型转换过程和方法进行深入研究的基础上,重点研究了软件体系结构模型及其间映射关系的形式化语义描述,以此为基础,对模型转换应保持的语义特性进行了分析和探讨,并开发了原型系统对研究成果进行了应用和验证。本文主要的研究内容和创新工作包括:（1）对模型转换过程和方法的研究。从模型描述语言的分析入手,讨论了模型转换和模型映射的一致性需求,并对模型转换的过程和已提出的模型转换方法进行了综述和归结。借助于形式语言的扩展机制,提出了基于概念集重构的模型映射定义方法,讨论了模型描述语言之间映射关系的建立过程以及所应遵循的基本原则,并重点分析了不同抽象层次结构模型之间的映射关系定义和转换的构造过程。依据体系结构模型的抽象定义,提出了基于体系结构映射的模型转换理论架构,从而为基于软件体系结构的模型转换一致性研究奠定了理论基础。（2）建立了体系结构模型及其映射关系的形式化语义描述方法。在对陆汝钤院士提出的类型范畴理论进行扩展的基础上,将其与代数规范和进程代数相结合,为软件体系结构模型以及模型间的映射关系提供了一种统一的语义描述框架。模型的结构语义由类型范畴图表来指代,行为语义则由范畴附带的进程行为迹来表示,模型间的映射关系用范畴理论中的态射和函子来形式化描述。该描述机制通用性强,通过将一系列小的局部映射的结果组合在一起形成大的复合结构,以一种渐增的方式来描述抽象模型到具体实现的转换关系,从而为局部映射的组合提供了一种可行的思路和方法。使用范畴理论作为数学框架,使得所讨论的问题可以用与特定应用领域无关的术语来形式化描述。范畴理论支持图形化建模,可以使模型中的构件关系以及结构特征可视化,有利于对模型转换的理解和追踪。应用研究表明,该描述框架很好地把握了模型驱动开发的实质、过程和要求,为模型转换和模型驱动的软件开发提供了新的认知、设计和语义计算的指导架构。本文是首次将类型范畴理论用于研究模型的组织结构和模型间的转换关系,将为其他学者研究软件模型的转换问题提供一种新的思路。（3）对体系结构模型转换所应保持的语义特性进行了研究。分析了模型转换过程中的语义迁移。基于软件体系结构模型的形式化描述,从结构语义、公理语义、端口语义和行为语义等几个方面分析了模型转换中特性保持问题的描述,并建立了相应的判定标准,同时探讨了证明一个转换是否满足某些特性保持约束的方法。这些方法支持以定理证明的方式,对模型转换的语义特性保持进行验证,克服了模型检测的不足。该研究可用于指导模型转换规则的定义,为模型映射关系的正确性验证提供依据,从而为进一步全面研究模型转换所应遵循的法则和特性奠定基础。本文是首次提出从体系结构模型之间的映射关系所表达的模型复合的语义的一致性来考察模型转换的正确性,在模型驱动开发研究领域是一次新的尝试。（4）在开发和应用方面,开发了模型驱动方法的原型工具,并完成了一系列的工程应用。从软件体系结构建模出发,通过对UML进行扩展,提出了一种包括体系结构模型、静态视图、逻辑视图和界面展示视图四部分的WEB应用模型描述方法。然后依据体系结构模型转换一致性研究的理论和方法定义模型转换规则,实现了向J2EE平台和ASP.NET平台的模型转换和代码生成,从而验证了本文所提理论和方法的合理性和实用性。本文的研究成果丰富和完善了MDD方法的理论架构,为模型驱动的软件开发研究提供了一种新的思路,对于促进MDD方法坚实、快速的发展,提升软件开发层次和提高开发效率,有重要和积极的推动作用。本文提出的语义描述框架丰富了软件体系结构形式化方法的研究,推动了范畴理论在计算机科学中的应用和发展,可以为从事范畴论方向的研究人员提供参考与启发。另外,类型范畴理论适合知识的抽象描述和知识处理,并且具备表达和推理能力,本文的工作还将有利于智能开发软件的研究。