The i*ToNuSMV Tool

The i*ToNuSMV tool is a Goal Oriented Requirements Engineering tool that bridges the gap between a sequence agnostic goal model (here i*) and the extended finite state machine that the NuSMV  model verifier takes as input. The tool helps requirement analysts by enabling them to perform model checking of goal models in the early requirements phase itself.

The tool takes an i* model as input and generates a NuSMV model that corresponds to the given i* model. This NuSMV model can be fed into the NuSMV model checker and verified against specific system properties that must be satisfied. These properties can be specified using temporal languages like CTL or LTL. The tool can be extensively used for checking compliance constraints in the requirements phase.

i*ToNuSMV Version 2.02: MAJOR UPGRADE. This is the first version of the tool that is functionally complete. It supports multiple actors as well as inter-actor dependencies. Also, this version generates one state transition model and one NuSMV input model for the given i* model. Thus, users are no longer restricted to perform model checking on a per actor basis.

  1.         Installer File
  2.         User Manual
  3.         Tutorial Video

Contributors: Ankita Bhaumik, Mandira Roy, Surochita Pal

i*ToNuSMV Version 2.01: MAJOR UPGRADE. The input language of the tool has been changed from the previous non-standardized textual input to tGRL (Vahdat Abdelzad, et. al., University of Ottawa).

  1.         Installer File
  2.         User Manual and Tutorial Video same as Version 1.04 (The user only has to write the input files using the tGRL textual notation. The working of the tool interface is same as the previous version.)

Contributors: Ankita Bhaumik, Mandira Roy, Surochita Pal, Soma Mallick

i*ToNuSMV Version 1.04: Bug fix. Previous version was path dependent. User compelled to install the tool in path “C:\istarToNuSMV”. Path dependency removed.

  1.         Installer File
  2.         User Manual and Tutorial Video same as Version 1.03

i*ToNuSMV Version 1.03: The NuSMV model verifier has been integrated into the tool. Users can now verify CTL specifications on the NuSMV model being generated.

  1. Installer File
  2. User Manual
  3. Tutorial Video

Contributors: Soma Mallick

i*ToNuSMV Version 1.02: This version accepts an i* model and only converts it to the corresponding finite state machine and NuSMV input model.

  1. Installer file
  2. User Manual
  3. Tutorial Video

Contributors: Nitesh Shukla

How to install the i*ToNuSMV tool:

Step-1: Double click on the downloaded istarToNusmv.msi file. The installation wizard opens as follows:


Step-2: Click on Next button. You will displayed the installation path settings:


Step-3: Keep the installation folder path as suggested. Click on Next to go to the verification dialog:


Step-4: Click on the Install button to begin the installation process:


Step-5: After successful installation the Finish dialog pops up. Check the Launch button to start using the tool: