SMT-based variability analyses in FeatureIDE

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

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

Abstrakt

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.
OriginalsprogEngelsk
TitelProceedings - VaMoS 2020 : 14th International Working Conference on Variability Modelling of Software-Intensive Systems
RedaktørerMaxime Cordy, Mathieu Acher, Danilo Beuche, Gunter Saake
Antal sider9
ForlagAssociation for Computing Machinery
Publikationsdatofeb. 2020
Artikelnummer6
ISBN (Elektronisk)978-1-4503-7501-6
DOI
StatusUdgivet - feb. 2020
Begivenhed14th International Working Conference on Variability Modelling of Software-Intensive Systems - Magdeburg, Tyskland
Varighed: 5. feb. 20207. feb. 2020

Konference

Konference14th International Working Conference on Variability Modelling of Software-Intensive Systems
Land/OmrådeTyskland
ByMagdeburg
Periode05/02/202007/02/2020

Fingeraftryk

Dyk ned i forskningsemnerne om 'SMT-based variability analyses in FeatureIDE'. Sammen danner de et unikt fingeraftryk.

Citationsformater