MSD-to-SMV for product lines

Modern technical systems today typically consist of multiple interacting components and very often not only a single product, but a whole product line with different compositions of components and functions must be developed. In joint work with Maxime Cordy and Patrick Heymans (Facultés Universitaires Notre-Dame de la Paix, Namur), Amir Sharifloo and I have developed a new tool for modeling and consistency checking scenario-based product line specifications.

The idea of this tool is that a requirements engineer can first define, by using a feature diagram, that different the variants of a product to consist of different compositions of features. A feature is a set of components and functions to be present in a system. Then, the components and the interactions of these components can be specified for each feature. We propose the interactions to be modeled with Modal Sequence Diagrams (MSDs), a recent variant of Live Sequence Charts (LSCs). Then, we can map a feature diagram and the MSD interaction specifications to a feature transition system encoded in SMV. By using an extension of the NuSMV model checker, we are then able to efficiently check the consistency of the scenario-based product line specification.

Find more information in the Tools section.