Model checking of extended OCL constraints on UML models in SOCLe

We present the first tool that offers dynamic verification of extended OCL constraints on UML models. It translates a UML model into an Abstract State Machine (ASM) which is transformed by an ASM simulator into an abstract structure called UML-valued OO TransitionSystem (OOTSUML). The Extended Object Constraints Language (EOCL) is interpreted on computation trees of this OOTSUML allowing for the statement of both OCL expressions modelling the system and OO primitives binding it to UML on the one hand, and safety or liveness constraints on the computation trees of the UML/OCL model on the other hand. An on-the-fly model checking algorithm, which provides the capability to work, at any time, on as small a possible subset of states as necessary, has been integrated into the tool.