Mixed strategy reasoning — an approach for resolution-based verification of OCL constraints in UML models
Imre Kilián · Pollack Periodica · 2007
The paper describes the SILK-Verifier component, a resolution-based verification tool for OCL constraints of UML static models. First, the projection of OCL constraints to first-order logic formulae is explained, then, the way of finding contradictions and inconsistencies in these formulae is shown. The concept of mixed strategy reasoning is introduced, i.e. the way to make the reasoning capabilities of several Constraint Logic Programming solvers to cooperate in an interacting manner. For the best understanding of the problem, a concrete example for the cooperation of solvers is presented. Finally, the experiences gained during the implementation are summarized.