UML-VT: UML Verification Tool

UML-VT is an open source Eclipse plug-in that verifies UML activities against given requirements using well-know model checker tools such UPPAAL, SPIN, and NuSMV, and an experimental model checker PES. UML-VT is meant to support the integration of model checking into a MDD process. The integration aims to facilitate the use formal verification in the early phases of the development, and to create an easy to use interface regardless of the users knowledge of formal methods. Furthermore, the integration leverages the higher abstraction of the development models in order to reduce the state explosion problem, thereby allowing the verification of more complex systems.

Documentation

Installation Guide

User Guide

Download

Sourceforge

Related Literature

Zamira  Daw, John Mangino and Rance Cleaveland, “UML-VT: A Formal Verification Environment for UML Activity Diagrams", in ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (Submitted - 2015).

Zamira  Daw and Rance Cleaveland, “Comparing model checkers for timed UML-Activity diagrams", in Science of Computer Programming (2015).

Zamira  Daw, Rance Cleaveland and Marcus Vetter, “ Integrating of model checking and UML based model-driven development for embedded systems”, in Proceedings of 13th International Workshop on Automated Verification of Critical Systems (AVOCS). 2013.

Zamira  Daw, Rance Cleaveland and Marcus Vetter, “ Formal verification of software-based medical devices considering medical guidelines”, in Proceedings of Computer Assisted Radiology and Surgery 27th International Congress and Exhibition (CARS). 2013.

For more information:

Rance Cleaveland

Zamira Daw