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

Formal transformation and verification of UML model based on specification Z

作　　者：张杨[1] 段富[1] 

机构地区：[1]太原理工大学计算机科学与技术学院,山西太原030024

出　　处：《计算机工程与设计》2013年第6期2031-2035,共5页Computer Engineering and Design

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

摘　　要：统一建模语言(UML)所建立的模型的正确性无法通过其本身进行形式化验证,为解决这个问题,根据UML模型的静态性质和动态模块行为两个方面提出结合形式化规格说明语言的模型形式化方案,以此为基础提出将UML目标模型转化为Z规格说明的形式化方法,并用Z-EVES工具形式化检测Z规格描述的正确性。通过实例分析验证了该方法的可行性。The correctness of the model which the UML builds can not access formal verification by its own. In order to solve the problem, based on the static property and dynamic part of the UML models, two aspects of methods are proposed combing formal specification language for model formalization. Formal methods for translating the UML to Z is given, and the Z/EVES is to verify the Z specification. By an example of an UML model translation and verification, the effectiveness of the method is showed.

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]