list of dots Digital Research Alliance of Canada logo  NSERC logo  University of Ottawa logo / UniversitĂ© d'Ottawa

User Manual    [Previous]   [Next]   

NuSMV

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.