基于Object-Z的带OCL约束的UML类图形式化描述  

Formal Specification of UML Class Diagram with OCL Constraints Based on Object-Z

作　　者：江春[1] 

机构地区：[1]苏州大学计算机科学与技术学院,江苏苏州215006

出　　处：《沈阳师范大学学报（自然科学版）》2008年第4期456-459,共4页Journal of Shenyang Normal University:Natural Science Edition

摘　　要：UML OCL是基于一阶谓词逻辑和集合论的形式化语言,用它对UML类图进行约束后类图便具备严格语法和精确语义,同时也具备了演绎验证的基本条件;但由于目前的建模工具还无法对缺乏精确语义的UML类图进行有效的演绎验证.因此提出了一种带OCL约束的UML类图通过Object-Z进行形式化描述的方法,这样便可以充分利用Object-Z强大的演绎验证能力来验证UML类图的正确性和是否具有某种性质等.UML OCL is a formal language based on first order logic and set theorems, after which constraints the class diagram, that has rigorous syntax and precise semantics, and has a basic qualification for formal verification; But all the current modeling tools haven＇ t verified UML class diagram without precise semantics, so the paper offers a method of Object-Z describing UML class diagram with OCL constraints, in order to verify whether UML class diagram is correct and whether has some kinds of property by sufficiently using much stronger capability of Object-Z deduction verification.

关 键 词：统一建模2.0 对象约束语言 形式化语言Object-Z 

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