list of dots University of Ottawa logo / Université d'Ottawa

User Manual    [Previous]   [Next]   


NuSMV is a formal method notation that can be used check properties of behaviour models using logic.

The Umple NuSMV generator generates statements that can be used to analyse properties of state machine models.

More information about NuSMV can be found at the Alloy project home page, or on the Wikipedia NuSMV page.

This generator is discussed in detail in Opeyemi Adesina's PhD thesis: Integrating Formal Methods with Model-Driven Engineering.