NuSMV GUI is an  open source tool that allows the graphical representation of Harel's statecharts and their automatic translation into the input language of the NuSVM model checker.

The tool allows also to import Stateflow models and to translate them into NuSMV.

NuSMV GUI features:

  • Modeling of Harel's statecharts
  • Statecharts communication modeling
  • Translation of statecharts into the input language of NuSMV
  • Verification of LTL and CTL formulae on the graphical models with NuSMV
  • NEW: Stateflow to NuSMV translation
    The tool is the result of the thesis performed by Silvia Lorenzini titled "Interfaccia Grafica per Model Checker NuSVM", extended with the thesis of Daniele Sbaraccani titled "Conversione da Stateflow a NuSMV GUI"
    Documentation Download:
  • Version 2.0 - Install Guide [Download]
  • Version 2.0 - Developer's Guide [Download]
  • Version 2.0 - Stateflow to NuSMV GUI translator (ITALIAN) [Download]
  • Version 1.0 - NuSMV GUI (ITALIAN) [Download]
  • Prototype - User's Guide (ITALIAN) [Download]
    Tool Download:
  • Version 2.0 - source code - Windows [Download]
  • Version 2.0 - binaries - Windows [Download]
  • Version 2.0 - source code- Linux [Download]
  • Version 2.0 - binaries- Linux [Download]
  • Version 1.0 - source code - Windows/Linux [Download]
  • Prototype - binaries - Windows [Download]
  • Prototype - binaries - Linux [Download]
    Sample models download: