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

摘要： 针对模型驱动的软件开发(MDSD)中语义特性保持的描述和验证等问题,基于类型范畴理论的形式化框架和进程代数理论,提出了一种软件结构模型的形式化描述方法。在此基础上对模型转换前后构件规范之间应满足的语义约束进行了深入的分析和探讨,从图表结构、端口与配置约束、外部行为以及可替换性等四个方面对特性约束保持的问题进行了描述,并建立了相应的判定标准。该方法能为模型之间转换规则的定义提供指导,并为模型转换的效果分析和正确性验证提供依据。应用研究表明,该方法使得构件模型的语义描述能力显著增强,可作为已有软件建模方法的一个有效补充。

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