Skip to content

MSD-to-SMV

We have implemented a tool which allows engineers to specify product lines through scenarios and to verify their consistency. The specifications are given in the form of UML models, which are then transformed into an fSMV model. Then, our NuSMV extension can be used to identify all the inconsistent products.

A more thorough presentation, installation instructions and guidelines for using the tool are provided in here.

This work is the result of a joint collaboration between the following people :

  • Joel Greenyer (Paderborn University, Politecnico di Milano)
  • Amir Molzam Sharifloo (Politecnico di Milano)
  • Maxime Cordy (University of Namur)
  • Patrick Heymans (University of Namur)