基于Z规格的UML模型形式化转换及验证

摘要：

统一建模语言(UML)所建立的模型的正确性无法通过其本身进行形式化验证,为解决这个问题,根据UML模型的静态性质和动态模块行为两个方面提出结合形式化规格说明语言的模型形式化方案,以此为基础提出将UML目标模型转化为Z规格说明的形式化方法,并用Z-EVES工具形式化检测Z规格描述的正确性.通过实例分析验证了该方法的可行性.

关键词：形式化方法、形式化验证、统一建模语言、Z规格、Z-EVES

所属期刊栏目：34

分类号：TP311.5(计算技术、计算机技术)

资助基金：山西省自然科学基金项目2008011039;山西省科技攻关基金项目20080322008

在线出版日期：2013-09-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：2031-2035