Using the Tool

(The MSD-to-SMV for Product Lines Tool)

If you’ve followed the installation instructions, there will now be the following two projects in your (runtime) workspace:

  • it.polimi.elet.deepse.msdtonusmv
  • it.polimi.elet.deepse.msdtonusmv.examples

The first project contains the transformation rules for transforming the UML scenario product line specifications to NuSMV models. The second contains a few examples specifications as well as their resulting NuSMV models. In the subfolders of the example project, you find the following files:

  • <specification-name>.uml
  • <specification-name>.umldi
  • <specification-name>.smv
  • <specification-name>.corr.xmi
  • <specification-name>.interpreterconfiguration

Now you can do the following:

Inspect or edit the UML scenario product line specifications

Open the *.umldi files with the TOPCASED UML editor that is extended with a special MSD editor. To open an MSD diagram, navigate to the interactions in the outline view and open the MSD diagram.

Inspect or edit the NuSMV models

Open *.smv (or *.nusmv) files with a syntax-highlighting MSD editor.

Check the consistency of the MSD product line specification

Call “NuSMV -fbdd <specification-name>.smv”.

Perform a MSD-to-SMV transformation

To perform a transformation of a UML scenario product line specification, the following steps are necessary. We distinguish between (1) changing an existing UML scenario product line specification and re-running an already configured transformation the transformation and (2) configuring a new transformation for a new UML scenario product line specification.

  1. Re-running a transformation: delete the .smv and.corr.xmi file and then right-click on the .interpreterconfiguration file->TGG-Interpreter->perform configured transformation. This should start a transformation. Hit “OK” on the two dialog windows that open after the transformation is finished to save the models. A new .smv file and another .corr.xmi file will be created.
  2. Creating a new transformation configuration: Select the .uml model and the it.polimi.elet.deepse.msdtonusmv\tgg\msdtonusmv.tgg file in your project explorer, right-click->TGG-Interpreter->create forward transformation interpreter configuration. This will create a .interpreterconfiguration file. The transformation can now be executed as described above. By default, however, the transformation will create a .NuSMV file, which will not be editable using the NuSMV text editor. To create a .smv text file, open the .interpreterconfiguration file with the TGG Interpreter configuration tree editor and navigate to the “Domain Model NuSMV”. Right-click and select “Show in Properties View” and then in the properties view change the appendix of the resource URI to be .smv instead of .NuSMV.