-
variability.dev: Towards an Online Toolbox for Feature Modeling
Authors:
Tobias Heß,
Lukas Ostheimer,
Tobias Betz,
Simon Karrer,
Tim Jannik Schmidt,
Pierre Coquet,
Sean Semmler,
Thomas Thüm
Abstract:
The emergence of feature models as the default to model the variability in configurable systems fosters a rich diversity in applications, application domains, and perspectives. Independent of their domain, modelers require to open, view, edit, transform, save, and configure models as well as to collaborate with others. However, at the time of writing, the top five results when googling ``Online Ed…
▽ More
The emergence of feature models as the default to model the variability in configurable systems fosters a rich diversity in applications, application domains, and perspectives. Independent of their domain, modelers require to open, view, edit, transform, save, and configure models as well as to collaborate with others. However, at the time of writing, the top five results when googling ``Online Editor Feature Model'' point to editors that either have minimal functionality, are unmaintained or defunct, or require an offline installation, such as FeatureIDE. In this work we present a preview of our in-development online toolbox for feature modeling, variability.dev. In particular, we showcase our collaborative feature-model editor and our online configurator both of which are built on top of the FeatureIDE library.
△ Less
Submitted 11 June, 2025;
originally announced June 2025.
-
Pseudo-Boolean d-DNNF Compilation for Expressive Feature Modeling Constructs
Authors:
Chico Sundermann,
Stefan Vill,
Elias Kuiter,
Sebastian Krieter,
Thomas Thüm,
Matthias Tichy
Abstract:
Configurable systems typically consist of reusable assets that have dependencies between each other. To specify such dependencies, feature models are commonly used. As feature models in practice are often complex, automated reasoning is typically employed to analyze the dependencies. Here, the de facto standard is translating the feature model to conjunctive normal form (CNF) to enable employing o…
▽ More
Configurable systems typically consist of reusable assets that have dependencies between each other. To specify such dependencies, feature models are commonly used. As feature models in practice are often complex, automated reasoning is typically employed to analyze the dependencies. Here, the de facto standard is translating the feature model to conjunctive normal form (CNF) to enable employing off-the-shelf tools, such as SAT or #SAT solvers. However, modern feature-modeling dialects often contain constructs, such as cardinality constraints, that are ill-suited for conversion to CNF. This mismatch between the input of reasoning engines and the available feature-modeling dialects limits the applicability of the more expressive constructs. In this work, we shorten this gap between expressive constructs and scalable automated reasoning. Our contribution is twofold: First, we provide a pseudo-Boolean encoding for feature models, which facilitates smaller representations of commonly employed constructs compared to Boolean encoding. Second, we propose a novel method to compile pseudo-Boolean formulas to Boolean d-DNNF. With the compiled d-DNNFs, we can resort to a plethora of efficient analyses already used in feature modeling. Our empirical evaluation shows that our proposal substantially outperforms the state-of-the-art based on CNF inputs for expressive constructs. For every considered dataset representing different feature models and feature-modeling constructs, the feature models can be significantly faster translated to pseudo-Boolean than to CNF. Overall, deriving d-DNNFs from a feature model with the targeted expressive constraints can be substantially accelerated using our pseudo-Boolean approach. Furthermore, our approach is competitive on feature models with only basic constructs.
△ Less
Submitted 9 May, 2025;
originally announced May 2025.
-
How Low Can We Go? Minimizing Interaction Samples for Configurable Systems
Authors:
Dominik Krupke,
Ahmad Moradi,
Michael Perk,
Phillip Keldenich,
Gabriel Gehrke,
Sebastian Krieter,
Thomas Thüm,
Sándor P. Fekete
Abstract:
Modern software systems are typically configurable, a fundamental prerequisite for wide applicability and reusability. This flexibility poses an extraordinary challenge for quality assurance, as the enormous number of possible configurations makes it impractical to test each of them separately. This is where t-wise interaction sampling can be used to systematically cover the configuration space an…
▽ More
Modern software systems are typically configurable, a fundamental prerequisite for wide applicability and reusability. This flexibility poses an extraordinary challenge for quality assurance, as the enormous number of possible configurations makes it impractical to test each of them separately. This is where t-wise interaction sampling can be used to systematically cover the configuration space and detect unknown feature interactions. Over the last two decades, numerous algorithms for computing small interaction samples have been studied, providing improvements for a range of heuristic results; nevertheless, it has remained unclear how much these results can still be improved.
We present a significant breakthrough: a fundamental framework, based on the mathematical principle of duality, for combining near-optimal solutions with provable lower bounds on the required sample size. This implies that we no longer need to work on heuristics with marginal or no improvement, but can certify the solution quality by establishing a limit on the remaining gap; in many cases, we can even prove optimality of achieved solutions. This theoretical contribution also provides extensive practical improvements: Our algorithm SampLNS was tested on 47 small and medium-sized configurable systems from the existing literature. SampLNS can reliably find samples of smaller size than previous methods in 85% of the cases; moreover, we can achieve and prove optimality of solutions for 63% of all instances. This makes it possible to avoid cumbersome efforts of minimizing samples by researchers as well as practitioners, and substantially save testing resources for most configurable systems.
△ Less
Submitted 12 January, 2025;
originally announced January 2025.
-
MulTi-Wise Sampling: Trading Uniform T-Wise Feature Interaction Coverage for Smaller Samples
Authors:
Tobias Pett,
Sebastian Krieter,
Thomas Thüm,
Ina Schaefer
Abstract:
Ensuring the functional safety of highly configurable systems often requires testing representative subsets of all possible configurations to reduce testing effort and save resources. The ratio of covered t-wise feature interactions (i.e., T-Wise Feature Interaction Coverage) is a common criterion for determining whether a subset of configurations is representative and capable of finding faults. E…
▽ More
Ensuring the functional safety of highly configurable systems often requires testing representative subsets of all possible configurations to reduce testing effort and save resources. The ratio of covered t-wise feature interactions (i.e., T-Wise Feature Interaction Coverage) is a common criterion for determining whether a subset of configurations is representative and capable of finding faults. Existing t-wise sampling algorithms uniformly cover t-wise feature interactions for all features, resulting in lengthy execution times and large sample sizes, particularly when large t-wise feature interactions are considered (i.e., high values of t). In this paper, we introduce a novel approach to t-wise feature interaction sampling, questioning the necessity of uniform coverage across all t-wise feature interactions, called \emph{\mulTiWise{}}. Our approach prioritizes between subsets of critical and non-critical features, considering higher t-values for subsets of critical features when generating a t-wise feature interaction sample. We evaluate our approach using subject systems from real-world applications, including \busybox{}, \soletta{}, \fiasco{}, and \uclibc{}. Our results show that sacrificing uniform t-wise feature interaction coverage between all features reduces the time needed to generate a sample and the resulting sample size. Hence, \mulTiWise{} Sampling offers an alternative to existing approaches if knowledge about feature criticality is available.
△ Less
Submitted 28 June, 2024;
originally announced June 2024.
-
Exploiting d-DNNFs for Repetitive Counting Queries on Feature Models
Authors:
Chico Sundermann,
Heiko Raab,
Tobias Heß,
Thomas Thüm,
Ina Schaefer
Abstract:
Feature models are commonly used to specify the valid configurations of a product line. In industry, feature models are often complex due to a large number of features and constraints. Thus, a multitude of automated analyses have been proposed. Many of those rely on computing the number of valid configurations which typically depends on solving a #SAT problem, a computationally expensive operation…
▽ More
Feature models are commonly used to specify the valid configurations of a product line. In industry, feature models are often complex due to a large number of features and constraints. Thus, a multitude of automated analyses have been proposed. Many of those rely on computing the number of valid configurations which typically depends on solving a #SAT problem, a computationally expensive operation. Further, most counting-based analyses require numerous #SAT computations on the same feature model. In particular, many analyses depend on multiple computations for evaluating the number of valid configurations that include certain features or conform to partial configurations. Instead of using expensive repetitive computations on highly similar formulas, we aim to improve the performance by reusing knowledge between these computations. In this work, we are the first to propose reusing d-DNNFs for performing efficient repetitive queries on features and partial configurations. Our empirical evaluation shows that our approach is up-to 8,300 times faster (99.99\% CPU-time saved) than the state of the art of repetitively invoking #SAT solvers. Applying our tool ddnnife reduces runtimes from days to minutes compared to using #SAT solvers.
△ Less
Submitted 22 March, 2023;
originally announced March 2023.
-
Flexible Correct-by-Construction Programming
Authors:
Tobias Runge,
Tabea Bordis,
Alex Potanin,
Thomas Thüm,
Ina Schaefer
Abstract:
Correctness-by-Construction (CbC) is an incremental program construction process to construct functionally correct programs. The programs are constructed stepwise along with a specification that is inherently guaranteed to be satisfied. CbC is complex to use without specialized tool support, since it needs a set of predefined refinement rules of fixed granularity which are additional rules on top…
▽ More
Correctness-by-Construction (CbC) is an incremental program construction process to construct functionally correct programs. The programs are constructed stepwise along with a specification that is inherently guaranteed to be satisfied. CbC is complex to use without specialized tool support, since it needs a set of predefined refinement rules of fixed granularity which are additional rules on top of the programming language. Each refinement rule introduces a specific programming statement and developers cannot depart from these rules to construct programs. CbC allows to develop software in a structured and incremental way to ensure correctness, but the limited flexibility is a disadvantage of CbC. In this work, we compare classic CbC with CbC-Block and TraitCbC. Both approaches CbC-Block and TraitCbC, are related to CbC, but they have new language constructs that enable a more flexible software construction approach. We provide for both approaches a programming guideline, which similar to CbC, leads to well-structured programs. CbC-Block extends CbC by adding a refinement rule to insert any block of statements. Therefore, we introduce CbC-Block as an extension of CbC. TraitCbC implements correctness-by-construction on the basis of traits with specified methods. We formally introduce TraitCbC and prove soundness of the construction strategy. All three development approaches are qualitatively compared regarding their programming constructs, tool support, and usability to assess which is best suited for certain tasks and developers.
△ Less
Submitted 6 June, 2023; v1 submitted 28 November, 2022;
originally announced November 2022.
-
T-Wise Presence Condition Coverage and Sampling for Configurable Systems
Authors:
Sebastian Krieter,
Thomas Thüm,
Sandro Schulze,
Sebastian Ruland,
Malte Lochau,
Gunter Saake,
Thomas Leich
Abstract:
Sampling techniques, such as t-wise interaction sampling are used to enable efficient testing for configurable systems. This is achieved by generating a small yet representative sample of configurations for a system, which circumvents testing the entire solution space. However, by design, most recent approaches for t-wise interaction sampling only consider combinations of configuration options fro…
▽ More
Sampling techniques, such as t-wise interaction sampling are used to enable efficient testing for configurable systems. This is achieved by generating a small yet representative sample of configurations for a system, which circumvents testing the entire solution space. However, by design, most recent approaches for t-wise interaction sampling only consider combinations of configuration options from a configurable system's variability model and do not take into account their mapping onto the solution space, thus potentially leaving critical implementation artifacts untested. Tartler et al. address this problem by considering presence conditions of implementation artifacts rather than pure configuration options, but do not consider the possible interactions between these artifacts. In this paper, we introduce t-wise presence condition coverage, which extends the approach of Tartler et al. by using presence conditions extracted from the code as basis to cover t-wise interactions. This ensures that all t-wise interactions of implementation artifacts are included in the sample and that the chance of detecting combinations of faulty configuration options is increased. We evaluate our approach in terms of testing efficiency and testing effectiveness by comparing the approach to existing t-wise interaction sampling techniques. We show that t-wise presence condition sampling is able to produce mostly smaller samples compared to t-wise interaction sampling, while guaranteeing a t-wise presence condition coverage of 100%.
△ Less
Submitted 30 May, 2022;
originally announced May 2022.
-
Traits for Correct-by-Construction Programming
Authors:
Tobias Runge,
Alex Potanin,
Thomas Thüm,
Ina Schaefer
Abstract:
We demonstrate that traits are a natural way to support correctness-by-construction (CbC) in an existing programming language in the presence of traditional post-hoc verification (PhV). With Correctness-by-Construction, programs are constructed incrementally along with a specification that is inherently guaranteed to be satisfied. CbC is complex to use without specialized tool support, since it ne…
▽ More
We demonstrate that traits are a natural way to support correctness-by-construction (CbC) in an existing programming language in the presence of traditional post-hoc verification (PhV). With Correctness-by-Construction, programs are constructed incrementally along with a specification that is inherently guaranteed to be satisfied. CbC is complex to use without specialized tool support, since it needs a set of refinement rules of fixed granularity which are additional rules on top of the programming language.
In this work, we propose TraitCbC, an incremental program construction procedure that implements correctness-by-construction on the basis of PhV by using traits. TraitCbC enables program construction by trait composition instead of refinement rules. It provides a programming guideline, which similar to CbC should lead to well-structured programs, and allows flexible reuse of verified program building blocks. We introduce TraitCbC formally and prove the soundness of our verification strategy. Additionally, we implement TraitCbC as a proof of concept.
△ Less
Submitted 12 April, 2022;
originally announced April 2022.
-
Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
Authors:
Alexander Knüppel,
Thomas Thüm,
Carsten Pardylla,
Ina Schaefer
Abstract:
Deductive verification of software has not yet found its way into industry, as complexity and scalability issues require highly specialized experts. The long-term perspective is, however, to develop verification tools aiding industrial software developers to find bugs or bottlenecks in software systems faster and more easily. The KeY project constitutes a framework for specifying and verifying sof…
▽ More
Deductive verification of software has not yet found its way into industry, as complexity and scalability issues require highly specialized experts. The long-term perspective is, however, to develop verification tools aiding industrial software developers to find bugs or bottlenecks in software systems faster and more easily. The KeY project constitutes a framework for specifying and verifying software systems, aiming at making formal verification tools applicable for mainstream software development. To help the developers of KeY, its users, and the deductive verification community, we summarize our experiences with KeY 2.6.1 in specifying and verifying real-world Java code from a users perspective. To this end, we concentrate on parts of the Collections-API of OpenJDK 6, where an informal specification exists. While we describe how we bridged informal and formal specification, we also exhibit accompanied challenges that we encountered. Our experiences are that (a) in principle, deductive verification for API-like code bases is feasible, but requires high expertise, (b) developing formal specifications for existing code bases is still notoriously hard, and (c) the under-specification of certain language constructs in Java is challenging for tool builders. Our initial effort in specifying parts of OpenJDK 6 constitutes a stepping stone towards a case study for future research.
△ Less
Submitted 27 November, 2018;
originally announced November 2018.
-
Proceedings 7th International Workshop on Formal Methods and Analysis in Software Product Line Engineering
Authors:
Julia Rubin,
Thomas Thüm
Abstract:
In Software Product Line Engineering (SPLE), a portfolio of similar systems is developed from a shared set of software assets. Claimed benefits of SPLE include reductions in the portfolio size, cost of software development and time to production, as well as improvements in the quality of the delivered systems. Yet, despite these benefits, SPLE is still in the early adoption stage. We believe that…
▽ More
In Software Product Line Engineering (SPLE), a portfolio of similar systems is developed from a shared set of software assets. Claimed benefits of SPLE include reductions in the portfolio size, cost of software development and time to production, as well as improvements in the quality of the delivered systems. Yet, despite these benefits, SPLE is still in the early adoption stage. We believe that automated approaches, tools and techniques that provide better support for SPLE activities can further facilitate its adoption in practice and increase its benefits.
To promote work in this area, the FMSPLE'16 workshop focuses on automated analysis and formal methods, which can (1) lead to a further increase in development productivity and reduction in maintenance costs associated with management of the SPLE artifacts, and (2) provide proven guarantees for the correctness and quality of the delivered systems.
△ Less
Submitted 28 March, 2016;
originally announced March 2016.
-
Leaf litter decomposition -- Estimates of global variability based on Yasso07 model
Authors:
M. Tuomi,
T. Thum,
H. Järvinen,
S. Fronzek,
B. Berg,
M. Harmon,
J. A. Trofymow,
S. Sevanto,
J. Liski
Abstract:
Litter decomposition is an important process in the global carbon cycle. It accounts for most of the heterotrophic soil respiration and results in formation of more stable soil organic carbon (SOC) which is the largest terrestrial carbon stock. Litter decomposition may induce remarkable feedbacks to climate change because it is a climate-dependent process. To investigate the global patterns of l…
▽ More
Litter decomposition is an important process in the global carbon cycle. It accounts for most of the heterotrophic soil respiration and results in formation of more stable soil organic carbon (SOC) which is the largest terrestrial carbon stock. Litter decomposition may induce remarkable feedbacks to climate change because it is a climate-dependent process. To investigate the global patterns of litter decomposition, we developed a description of this process and tested the validity of this description using a large set of foliar litter mass loss measurements (nearly 10 000 data points derived from approximately 70 000 litter bags). We applied the Markov chain Monte Carlo method to estimate uncertainty in the parameter values and results of our model called Yasso07. The model appeared globally applicable. It estimated the effects of litter type (plant species) and climate on mass loss with little systematic error over the first 10 decomposition years, using only initial litter chemistry, air temperature and precipitation as input variables. Illustrative of the global variability in litter mass loss rates, our example calculations showed that a typical conifer litter had 68% of its initial mass still remaining after two decomposition years in tundra while a deciduous litter had only 15% remaining in the tropics. Uncertainty in these estimates, a direct result of the uncertainty of the parameter values of the model, varied according to the distribution of the litter bag data among climate conditions and ranged from 2% in tundra to 4% in the tropics. This reliability was adequate to use the model and distinguish the effects of even small differences in litter quality or climate conditions on litter decomposition as statistically significant.
△ Less
Submitted 4 June, 2009;
originally announced June 2009.
