中文摘要：

语义一致性是模型驱动开发中模型转换正确性的一个重要标准,但目前模型转换中语义特性保持的定义、描述和验证仍是一个尚未解决的难题.基于软件体系结构,利用范畴理论和代数规范形式化描述体系结构模型及其间的映射关系,使之具有精确的语义.体系结构模型的形式化语义用类型范畴图表来表示,态射合成被用来追踪构件模型之间的关联和映射,不同层次模型间的映射关系用态射和函子来形式化描述.以此为基础,进一步分析了模型转换应保持的语义特性.范畴理论支持图形化建模,可以使模型中的构件关系以及结构特征可视化,有利于对模型转换的理解和追踪.应用研究表明,该描述框架很好地把握了模型驱动开发的实质、过程和要求,为模型转换和模型驱动开发提供了新的认知、设计和语义计算的指导架构.

英文摘要：

Semantic consistency between source models and target models is an important criterion of the correctness of model transformations in model-driven software development. However, the definition, description, and proof of semantic property preservation of model transformations are still problems unresolved. On the basis of software architecture, category theory and algebraic specification are combined together to provide precise semantics for architecture models and their mapping relations in this paper. Formal semantics of component specifications and architecture models are described within typed category diagrams. Morphism composition is used to trace the interconnections and mapping relations between component models, and the mapping relations between different levels of architecture models are formally described by morphisms and functors. On this basis, the semantic properties that should be preserved through model transformations are discussed subsequently. Category theory supports the diagrammatic representation of component models that visualizes the relationships among components and the structural features, which can be used to strengthen the understandability and traceability of model transformations. The application research shows that the framework captures the essence, process and requirements of model-driven development, and thus can be used as a new theoretical guidance for the cognition, design and semantic calculation of model transformations and model-driven software development.