Skip to main content

IBM UML Model Verifier (MoV)

MoV is a Rhapsody plug-in making formal verification technology available for behavioral UML designs. It analyses UML state machine and verifies properties of these machines, such as deadlock, mutual exclusion, invariants, and more. MoV is fully automatic and will provide either a guarantee that the property holds or a sequence diagram showing how the property fails to hold. It should be noted that while the tool's front-end is connected to Rhapsody, it is capable of working on any standard UML2 design.


Contact: Karen Yorav