SMT-based variability analyses in FeatureIDE

Joshua Sprey, Chico Sunderman, Sebastian Krieter, Michael Nieke, Jacopo Mauro, Thomas Thum, Ina Schaefer

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

Handling configurable systems with thousands of configuration options is a challenging problem in research and industry. One of the most common approaches to manage the configuration options of large systems is variability modelling. The verification and configuration process of large variability models is manually infeasible. Hence, they are usually assisted by automated analyses based on solving satisfiability problems (SAT). Recent advances in satisfiability modulo theories (SMT) could prove SMT solvers as a viable alternative to SAT solvers. However, SMT solvers are typically not utilized for variability analyses. A comparison for SAT and SMT could help to estimate SMT solvers potential for the automated analysis. We integrated two SMT solvers into FeatureIDE and compared them against a SAT solver on analyses for feature models, configurations, and realization artifacts. We give an overview of all variability analyses in FeatureIDE and present the results of our empirical evaluation for over 122 systems. We observed that SMT solvers are generally faster in generating explanations of unsatisfiable requests. However, the evaluated SAT solver outperformed SMT solvers for other analyses.
Original languageEnglish
Title of host publicationProceedings - VaMoS 2020 : 14th International Working Conference on Variability Modelling of Software-Intensive Systems
EditorsMaxime Cordy, Mathieu Acher, Danilo Beuche, Gunter Saake
Number of pages9
PublisherAssociation for Computing Machinery
Publication dateFeb 2020
Article number6
ISBN (Electronic)978-1-4503-7501-6
DOIs
Publication statusPublished - Feb 2020
Event14th International Working Conference on Variability Modelling of Software-Intensive Systems - Magdeburg, Germany
Duration: 5. Feb 20207. Feb 2020

Conference

Conference14th International Working Conference on Variability Modelling of Software-Intensive Systems
Country/TerritoryGermany
CityMagdeburg
Period05/02/202007/02/2020

Keywords

  • Attribute optimization
  • Configuration analysis
  • Feature attributes
  • Feature model analysis
  • Feature models
  • Preprocessor analysis
  • SMT
  • SMT analysis
  • Sat
  • Sat analysis
  • Sat vs SMT
  • Variability analysis

Fingerprint

Dive into the research topics of 'SMT-based variability analyses in FeatureIDE'. Together they form a unique fingerprint.

Cite this