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 Transition System (OOTS UML ). The Extended Object Constraints Language (EOCL) is interpreted on computation trees of this OOTS UML , 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.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Mullins, John; Oarga, Raveca: Model checking of extended OCL constraints on UML models in SOCLE (2007)