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

Formal specification of UML class diagram with OCL constraints based on Object-Z

作　　者：江春[1] 

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

出　　处：《沈阳工程学院学报（自然科学版）》2008年第4期372-375,共4页Journal of Shenyang Institute of Engineering:Natural Science

摘　　要：UML2.0 OCL是基于一阶谓词逻辑和集合论的形式化语言,用它对UML类图进行条件约束后,类图便具备了严格的语法和精确的语义,同时也具备了演绎验证的基本条件.但由于目前的建模工具还无法对缺乏精确语义的UML类图进行有效的演绎验证,因此提出了将带OCL约束的UML类图通过Object-Z进行形式化描述的方法,这样便可以充分利用Object-Z强大的演绎验证能力来验证UML类图的正确性和是否具有某种性质等。UML2.00CL is a formal language based on first-order predict logic and set theorems, by which the UML class diagram are constrained and the diagram has rigorous syntax and precise semantics, and has a basic qualification for forreal verification. But all the current modeling tool 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语言 

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