关键词：UML序列图;UML状态图;机械语义;精化;定理证明器Coq;元模型
摘 要：如今的软件系统已经广泛应用于人们日常生活的各个领域,然而,开发出可靠和正确的软件系统依然是一个巨大的挑战。形式化方法使用基于数学符号的形式规范描述系统,使得设计开发人员能够对系统进行严格的形式化描述、分析和验证,提高系统的可靠性和正确性。模型驱动工程作为当前工业界主流的软件系统开发方法,主要理念也是要提高开发的抽象层次,将模型作为核心,强调规范语言、分析方法和工具的实用性,确保软件的行为是适当的和正确的。作为模型驱动工程的重要组成部分,统一建模语言UML已经成为业界用于建模的事实标准,却因为本身缺乏精确的形式语义定义,使得对UML模型进行形式验证变得十分的困难。更重要地,软件设计通常是个增量迭...
内 容：原文可通过湖北省科技信息共享服务平台（http://www.hbstl.org.cn)获取