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

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

采用形式化方法对软件模型进行自动验证在模型驱动架构开发方法中发挥重要的作用.本文提出一种对面向对象软件设计模型的静态结构进行验证的具体实现方法.该方法将用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.