NuSMV is a symbolic model checker
NuSMV is a reimplementation and extension of SMV, the first model checker based on BDDs. NuSMV has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques, and applied to other research areas.
NuSMV2, combines BDD-based model checking component that exploits the CUDD library developed by Fabio Somenzi at Colorado University and SAT-based model checking component that includes an RBC-based Bounded Model Checker, connected to the SIM SAT library developed by the University of Genova.
G. Engels, J. Küster, R. Heckel, and M. Lohmann. Electr. Notes Theor. Comput. Sci., (2003)MR: UML-Modell (On the high level, our system model is composed of use case diagrams and sequence diagrams describing the interaction of the system with users of the system. On the low level, it is composed of class diagrams, statecharts and activity diagrams.) wird durch Grapftransformationen in eine formale Sprache (CSP) überführt und mit einem Model-Checker validiert und in ein Testmodell überführt..