-
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 map** 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) develo** 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 step** 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.
