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 language | English |
---|---|
Title of host publication | Proceedings - VaMoS 2020 : 14th International Working Conference on Variability Modelling of Software-Intensive Systems |
Editors | Maxime Cordy, Mathieu Acher, Danilo Beuche, Gunter Saake |
Number of pages | 9 |
Publisher | Association for Computing Machinery |
Publication date | Feb 2020 |
Article number | 6 |
ISBN (Electronic) | 978-1-4503-7501-6 |
DOIs | |
Publication status | Published - Feb 2020 |
Event | 14th International Working Conference on Variability Modelling of Software-Intensive Systems - Magdeburg, Germany Duration: 5. Feb 2020 → 7. Feb 2020 |
Conference
Conference | 14th International Working Conference on Variability Modelling of Software-Intensive Systems |
---|---|
Country/Territory | Germany |
City | Magdeburg |
Period | 05/02/2020 → 07/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