Sciweavers

Share
FMOODS
2007

Model Checking of Extended OCL Constraints on UML Models in SOCLe

8 years 10 months ago
Model Checking of Extended OCL Constraints on UML Models in SOCLe
We present the first tool that offers dynamic verification of extended traints on UML models. It translates a UML model into an Abstract State (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.
John Mullins, Raveca Oarga
Added 29 Oct 2010
Updated 29 Oct 2010
Type Conference
Year 2007
Where FMOODS
Authors John Mullins, Raveca Oarga
Comments (0)
books