Summary of: On the Expressiveness of Modal Transition Systems with Variability Constraints

摘要

Modal transition systems (MTSs) and featured transition systems (FTSs) are widely recognised as fundamental behavioural models for software product lines. This short paper summarises the contributions published in [3]: MTSs with variability constraints (MTSvs) are equally expressive as FTSs. This is proved by giving sound and complete transformations of the latter into the former, and of the former into the latter. The benefits of this result are twofold. First, it contributes to the expressiveness hierarchy of such basic models studied in the literature. Second, it provides an automatic algorithm from FTSs to MTSus that preserves the original (compact) branching structure, thus paving the way for model checking FTSs with the variability model checker VMC.