Formal Semantics of Component-Based Architecture Model Mapping

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.