关键词：UML;模型转换;元模型;Coq定理证明器;机械语义
摘 要：作为当今的主流建模语言,统一建模语言UML被广泛应用于软件生命周期的各个阶段。然而,UML本身是一种图形化的语言,不具有形式化的语义。缺乏精确的语义,导致UML建模工具一般不具有模型分析和验证等功能,使得其对验证及自动分析的支持能力显得不足。机械语义作为形式化语义的一种,通过使语义机械化,能够消除自然语言或图形语言定义的语义规范的歧义,并且可以在定理证明器中对模型的语义进行严格的定义、分析和验证。如果能够获得UML模型的机械语义,就能通过定理证明器对UML模型进行分析和验证,从而提高设计阶段UML模型的正确性和可靠性。然而,UML模型到定理证明器内置的形式语言的映射规则通常难以定义,需要开发者...
内 容：原文可通过湖北省科技信息共享服务平台（http://www.hbstl.org.cn)获取