Date Added: Sep 2010
There is a need for more rigorous analysis techniques that developers can use for verifying the critical properties in UML models. The UML-based Specification Environment (USE) tool supports verification of invariants, pre-conditions, and post-conditions specified in the Object Constraint Language (OCL). Due to its animation and analysis power, it is useful when checking critical non-functional properties such as security policies. However, the USE requires one to specify a model using its own textual language and does not allow one to import any model specification files created by other UML modeling tools. Hence, one would create a model with OCL constraints using a modeling tool such as the IBM Rational Software Architect (RSA) and then use the USE for the model verification.