一种利用Kodkod约束求解器验证UML-OCL类图的方法  

An Approach for Exploiting Kodkod Constraint Solver to Verify UML-OCL Class Diagrams

作　　者：罗奇鸣[1] 

机构地区：[1]中国科学技术大学计算机科学与技术学院

出　　处：《小型微型计算机系统》2014年第2期205-209,共5页Journal of Chinese Computer Systems

基　　金：MOE-MS多媒体计算与通信实验室基金项目(07122807)资助

摘　　要：采用形式化方法对软件模型进行自动验证在模型驱动架构开发方法中发挥重要的作用.本文提出一种对面向对象软件设计模型的静态结构进行验证的具体实现方法.该方法将用OCL不变式约束的UML类图转换为用关系逻辑表达的公式,Kodkod约束求解器可对关系逻辑公式进行验证.本文方法克服了文献中类似方法的局限性,即在允许类图中出现多重继承和关联重数的上下界为任意整数的同时无需大的计算代价.Verifying software models by formal methods plays an important role in model driven architecture. This paper proposes a detailed implementation approach for verifying structural models of object-oriented software. UML class diagrams constrained by OCL invariants are transformed into relational logic formula, which can be verified by the Kodkod constraint solver. Our approach over- comes the limitations of similar approaches in the literature by supporting multiple inheritance and allowing arbitrary integers in the multiplicities of associations without incurring excessive computational cost.

关 键 词：统一建模语言 对象约束语言 类图 验证 软件工程 

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