摘要：As semantic consistency becomes the most important criterion of the correctness of model transformations in model-driven software development, the definition, description, and proof of semantic property preservation become crucial. This paper extends typed category theory to provide a formal description approach for architecture model transformation. Category diagrams are used to provide formal semantics of component specifications and architecture models. The transformation between different levels of models is formally described by morphisms. The approach can be used for the description, analysis and judgment of property preservation to strengthen the understandability and traceability of model transformations. The application research shows that the approach captures the essence, process and requirements of model transformation, and thus can make an effective support for model-driven software development.
关键词：formal approach;model transformation;software architecture;component model
