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.

AGTIVE 2011 paper accepted for publication

The paper Applying Advanced TGG Concepts for a Complex Transformation of Sequence Diagram Specifications to Timed Game Automata, written in collaboration with Jan Rieke, was accepted for publication.

We presented the paper already last October at the AGTIVE Symposium. The paper describes a number of extension that we have implemented into the TGG Interpreter in the last years in order to apply the tool to a broader range of practically relevant transformation problems. A draft version of the paper can be found here.