Mahsa Varshosaz, Lars Luthmann, Paul Mohr, Malte Lochau, and Mohammad Reza Mousavi

Featured transition systems (FTSs) and modal transition systems (MTSs) are two of the most prominent and well-studied formalisms for modeling and analyzing behavioral variability as apparent in software product line engineering. On one hand, it is well-known that for finite behavior FTSs are strictly more expressive than MTSs, essentially due to the inability of MTSs to express logically constrained behavioral variability such as persistently exclusive behaviors. On the other hand, MTSs enjoy many desirable formal properties such as compositionality of semantic refinement and parallel composition. In order to finally consolidate the two formalisms for variability modeling, we establish a rigorous connection between FTSs and MTSs by means of an encoding of one FTS into an equivalent set of multiple MTSs. To this end, we split the structure of an FTS into several MTSs whenever it is necessary to denote exclusive choices that are not expressible in a single MTS. Moreover, extra care is taken when dealing with infinite behaviour: loops may have to be unrolled to accumulate FTS path constraints when encoding them into MTSs. We prove our encoding to be semantic-preserving (i.e., the resulting set of MTSs induces, up to bisimulation, the same set of derivable variants as their FTS counterpart) and to commute with modal refinement. We further give an algorithm to calculate a concise representation of a given FTS as a minimal set of MTSs. Finally, we present experimental results gained from applying a tool implementation of our approach to a collection of case studies.

We performed an experimental evaluation to illustrate the potential and feasability of our approach. The central parts of our replication package can be found here:

Note: Some programs (e.g., Microsoft Excel) do not correctly display the content of the .csv-files. For analyzing the results of our evaluation, we therefore used LibreOffice.

In order to reproduce the results of our experimental evaluation, we presume that you have a machine with OpenJDK 1.8 (or compatible) being installed. To generate a set of MTS from one of our case studies, first open the JAR-file and scroll down to the bottom of the main window. Here, you may enter a configString (i.e., a string containing all information of an FTS as well as the corresponding feature model) of a case study. The respective strings for all of our case studies are listed in the files containing the raw data. After pasting the configString into the tool, press Import (below the string) and then Convert to MTS (above the string). For a more detailed description of our tool, we refer the reader to the manual of our tool.