关键词: 模型驱动的软件开发, 模型转换, 特性描述, 语义验证

Abstract: To resolve the problems on description and proof of semantic property preservation in Model-Driven Software Development (MDSD), a formal approach was proposed for software architecture model on the basis of type category theory and process algebra. The semantic constraints of component specifications which should be kept through model transformation, were deeply analyzed and discussed. From the view of diagram structure, port and configuration constraints, external behavior and component substitutability, the problem of property preservation was described, and the corresponding criteria was built at the same time. The framework provides a guidance for the definition of model transformation rules, and provides the basis to verify the correctness of model transformation as well as to analyze the effect of model transformation. The application research shows that, the approach enhances semantic description capabilities of component model, and can be used as an effective supplement for existing software modeling method.

Key words: Model-Driven Software Development (MDSD), model transformation, property description, semantic verification