Optimized Translation of Clafer Models to Alloy
B Kacper · 2011
Clafer is a textual language for modeling and analysis of software product lines. The language is able to express a wide range of models: feature models, meta-models, and feature-based model templates. Reasoning about those models is required to verify their consistency, detect dead elements, or to guide the configuration process for end-users. Clafer uses the Alloy Analyzer as a back-end to perform analyses on variability models. This paper presents how optimized translation rules of Clafer models to Alloy simplified the Alloy models and improved reasoning performance. The work was evaluated on publicly available feature models, slices of metamodels, and feature-based model templates. The results showed that the improved translation shortened reasoning time at least 2 times. The improvement by factor of 4 was not uncommon.