Software is typically configurable by means of compile-time or runtime variability. As testing every valid configuration is infeasible, T-Wise sampling has been proposed to systematically derive a relevant subset of the configurations for testing to cover interactions among t features. Practitioners started to apply T-Wise sampling algorithms, but can often only test samples partially due to restricted resources and compare those partial samples based on their T-Wise coverage. However, there is no consensus in the literature on how to compute the T-Wise coverage in the literature. We propose the first systematic framework to define coverage metrics for T-Wise feature interactions. These metrics differ in the features and feature interactions being considered. We found evidence for at least six different metrics in the literature. In an empirical evaluation, we show that for a partial sample the coverage differs up to 21 % and for some metrics only half of the feature interactions need to be covered. As a long-term impact, our work may help to improve the efficiency and effectiveness of both, T-Wise sampling and coverage computations.

Abstract In many recent application domains, software systems must repeatedly reconfigure themselves at runtime to satisfy changing contextual requirements. To decide which next configuration is presumably best suited is a very challenging task as it involves not only functional requirements but also non-functional properties (NFP). NFP include multiple, potentially contradicting, criteria like real-time constraints and cost measures like energy consumption. Effectiveness of context-aware reconfiguration decisions further depends on mostly uncertain future contexts which makes greedy one-step decision heuristics potentially misleading. Moreover, the computational runtime overhead for reconfiguration planning should not nullify the benefits. Nevertheless, entirely pre-planning reconfiguration decisions during design time is also not feasible due to missing knowledge about runtime contexts. In this article, we propose a model-based technique for precomputing context-aware reconfiguration decisions under partially uncertain real-time constraints and cost measures. We employ a game-theoretic approach based on stochastic priced timed game automata as reconfiguration model. This formal model allows us to automatically synthesize winning strategies for the first player (the system) which efficiently delivers presumably best-fitting reconfiguration decisions as reactions to moves of the second player (the context) at runtime. Our tool implementation copes with the high computational complexity of strategy synthesis by utilizing the statistical model checker Uppaal Stratego to approximate near-optimal solutions. We applied our tool to a real-world example consisting of a reconfigurable robot support system for the construction of aircraft fuselages. Our evaluation results show that Uppaal Stratego is indeed able to precompute effective reconfiguration strategies within a reasonable amount of time.

timeaware reconfiguration strategies based on stochastic priced timed games", written by Hendrik Göttmann, Birte Caesar,

Many modern software systems continuously reconfigure themselves to (self-)adapt to ever-changing environmental contexts. Selecting presumably best-fitting next configurations is, however, very challenging, depending on functional and non-functional criteria like real-time constraints as well as inherently uncertain future contexts which makes greedy one-step decision heuristics ineffective. In addition, the computational overhead caused by reconfiguration planning at run-time should not outweigh its benefits. On the other hand, completely pre-planning reconfiguration decisions at design time is also infeasible due to the lack of knowledge about the context behavior. In this paper, we propose a game-theoretic setting for precomputing reconfiguration decisions under partially uncertain real-time behavior. We employ stochastic timed game automata as reconfiguration model to derive winning strategies which enable the first player (the system) to make fast look-ups for presumably best-fitting reconfiguration decisions satisfying the second player (the context). To cope with the high computational complexity of finding winning strategies, our tool implementation1 utilizes the statistical model-checker Uppaal Stratego to approximate near-optimal solutions. In our evaluation, we investigate efficiency/effectiveness trade-offs by considering a real-world example consisting of a reconfigurable robot support system for the construction of aircraft fuselages.

Abstract The management of modern enterprise applications is automated by coordinating the deployment, configuration, enactment, and termination of their components. Choosing among different candidate implementations for a specified application component requires such implementations to conform to the specified management behaviour. This holds especially if we wish to ensure that the overall application management can continue as planned, or that no additional (potentially undesired) management activity gets enabled. To this end, we introduce a formal framework for testing “management conformance”, i.e., to test whether a candidate implementation can be managed according to the management protocol specifying the allowed management for a component. We also illustrate how our framework enables to run four different conformance tests, each providing a different trade-off between implementation freedom and guarantees on the overall application management. We formally prove that testing management conformance with constraints reducing implementation freedom results in preserving all already allowed management activities when implementing a specification by choosing a conforming implementation and that no additional (potentially undesired) management activity gets enabled. Finally, we assess our framework by means of a prototype implementation and its use in an experimental evaluation.

Abstract Software model checkers can be used to generate high-quality test cases from counterexamples of a reachability analysis. However, naïvely invoking a software model checker for each test goal in isolation does not scale to large programs as a repeated construction of an abstract program model is expensive. In contrast, invoking a software model checker for reaching all test goals in a single run leads to few abstraction possibilities and thus to low scalability. Therefore, our approach pursues a test-suite generation technique that incorporates configurable multi-goal set partitioning (MGP) including configurable partitioning strategies and simultaneous processing of multiple test goals in one reachability analysis. Our approach employs recent techniques from multi-property verification in order to control the computational overhead for tracking multi-goal reachability information. Our tool, called CPA/Tiger-MGP, uses predicate-abstraction-based program analysis in the model-checking framework CPAchecker.

In theory, software model checkers are well-suited for automated test-case generation. The idea is to perform (non-)reachability queries for the test goals and extract test cases from resulting counterexamples. However, in case of realistic programs, even simple coverage criteria (e.g., branch coverage) force model checkers to deal with several hundreds or even thousands of test goals. Processing each of these test goals in isolation with model checking techniques does not scale. Therefore, our tool HybridTiger builds on recent ideas on multi-property verification. However, since every additional property (i.e., test goal) reduces the model checker’s abstraction possibilities, we split the set of all test goals into different partitions. In Test-Comp 2019, we applied a random partitioning strategy and used predicate analysis as model checking technique. In Test-Comp 2020, we improved our technique in two ways. First, we exploit domination information among control-flow locations in our partitioning strategy to group test goals being located on (preferably) similar paths. Second, we account to inherent weaknesses of the predicate analysis by applying a hybrid software model-checking approach that switches between explicit model checking and predicate-based model checking on-the-fly. Our tool HybridTiger is integrated into the software analysis framework CPAchecker .

Modern software often exists in many different, yet similar versions and/or variants, usually derived from a common code base (e.g., via clone-and-own). In the context of product-line engineering, family-based analysis has shown very promising potential for improving efficiency in applying quality-assurance techniques to variant-rich software, as compared to a variant-by-variant approach. Unfortunately, these strategies rely on a product-line representation superimposing all program variants in a syntactically well-formed, semantically sound and variant-preserving manner, which is manually hard to obtain in practice. We demonstrate the SiMPOSE methodology for automatically generating superimpositions of N given program versions and/or variants facilitating family-based analysis of variant-rich software. SiMPOSE is based on a novel N-way model-merging technique operating at the level of control-flow automata (CFA) representations of C programs. CFAs constitute a unified program abstraction utilized by many recent software-analysis tools. We illustrate different merging strategies supported by SiMPOSE, namely variant-by-variant, N-way merging, incremental 2-way merging, and partition-based N/2-way merging, and demonstrate how SiMPOSE can be used to systematically compare their impact on efficiency and effectiveness of family-based unit-test generation. The SiMPOSE tool, the demonstration of its usage as well as related artifacts and documentation can be found at http://pi.informatik.uni-siegen.de/projects/variance/simpose.

Nowadays software tends to come in many different, yet similar variants, often derived from a common code base via clone-and-own. Family-based-analysis strategies have recently shown very promising potential for improving efficiency in applying quality-assurance techniques to such variant-rich programs, as compared to variant-by-variant approaches. Unfortunately, these strategies require a single program representation superimposing all program variants in a syntactically well-formed, semantically sound, and variant-preserving manner, which is usually not available and manually hard to obtain in practice. In this article, we present a novel methodology, called S i MPOSE, for automatically generating superimpositions of existing program variants to facilitate family-based analyses of variant-rich software. To this end, we propose a novel N-way model-merging methodology to integrate the control-flow automaton (CFA) representations of N given variants of a C program into one unified CFA representation. CFA constitute a unified program abstraction used by many recent software-analysis tools for automated quality assurance. To cope with the inherent complexity of N-way model-merging, our approach (1) utilizes principles of similarity-propagation to reduce the number of potential N-way matches, and (2) enables us to decompose a set of N variants into arbitrary subsets and to incrementally derive an N-way superimposition from partial superimpositions. We apply our tool implementation of S i MPOSE to a selection of realistic C programs, frequently considered for experimental evaluation of program-analysis techniques. In particular, we investigate applicability and efficiency/effectiveness trade-offs of our approach by applying S i MPOSE in the context of family-based unit-test generation as well as model-checking as sample program-analysis techniques. Our experimental results reveal very impressive efficiency improvements by an average factor of up to 2.6 for test-generation and up to 2.4 for model-checking under stable effectiveness, as compared to variant-by-variant approaches, thus amortizing the additional effort required for merging. In addition, our results show that merging all N variants at once produces, in almost all cases, clearly more precise results than incremental step-wise 2-way merging. Finally, our comparison with major existing N-way merging techniques shows that S i MPOSE constitutes, in most cases, the best efficiency/effectiveness trade-off.

Refactorings constitute an effective means to improve quality and maintainability of evolving object-oriented programs. Search-based techniques have shown promising results in finding optimal sequences of behavior-preserving program transformations that (1) maximize code-quality metrics and (2) minimize the number of changes. However, the impact of refactorings on extra-functional properties like security has received little attention so far. To this end, we propose as a further objective to minimize the attack surface of programs (i.e., to maximize strictness of declared accessibility of class members). Minimizing the attack surface naturally competes with applicability of established MoveMethod refactorings for improving coupling/cohesion metrics. Our tool implementation is based on an EMF meta-model for Java-like programs and utilizes MOMoT, a search-based model-transformation framework. Our experimental results gained from a collection of real-world Java programs show the impact of attack surface minimization on design-improving refactorings by using different accessibility-control strategies. We further compare the results to those of existing refactoring tools.

Recent research on quality assurance (QA) of configurable software systems (e.g., software product lines) proposes different analysis strategies to cope with the inherent complexity caused by the well-known combinatorial-explosion problem. Those strategies aim at improving efficiency of QA techniques like software testing as compared to brute-force configuration-by-configuration analysis. Sampling constitutes one of the most established strategies, defining criteria for selecting a drastically reduced, yet sufficiently diverse subset of software configurations considered during QA. However, finding generally accepted measures for assessing the impact of sample-based analysis on the effectiveness of QA techniques is still an open issue. We address this problem by lifting concepts from single-software mutation testing to configurable software. Our framework incorporates a rich collection of mutation operators for product lines implemented in C to measure mutation scores of samples, including a novel family-based technique for product-line mutation detection. Our experimental results gained from applying our tool implementation to a collection of subject systems confirms the widely-accepted assumption that pairwise sampling constitutes the most reasonable efficiency/effectiveness trade-off for sample-based product-line testing.

Clafer combines UML-like class- and meta-modeling with feature-oriented variability-modeling and first-order logic constraints. The considerable expressiveness of Clafer mainly stems from its built-in variability constructs, multiplicity annotations and recursive model structures which yield a potentially unbounded number of valid model instances. As a result, automated reasoning about semantic properties like model consistency (i.e., existence of valid model instances) and anomalies (e.g., false cardinality bounds) is very challenging. Recent analysis techniques are inherently incomplete as they impose an a-priori finite search space with either manually or heuristically adjusted bounds. In this paper, we present a novel approach for automated search-space restriction for a considerably rich, yet decidable fragment of the Clafer language that guarantees sound and complete detection results for a wide range of semantic anomalies. Our approach employs principles from mathematical programming by encoding Clafer models as Mixed Integer Linear Programs (MILP). Our experimental evaluation shows remarkable improvements of runtime efficiency as well as effectiveness of anomaly detection as compared to existing techniques.

A software product line comprises a family of software products that share a common set of features. It enables customers to compose software systems from a managed set of features. Testing every product of a product line individually is often infeasible due to the exponential number of possible products in the number of features. Several approaches have been proposed to restrict the number of products to be tested by sampling a subset of products achieving sufficient combinatorial interaction coverage. However, existing sampling algorithms do not scale well to large product lines, as they require a considerable amount of time to generate the samples. Moreover, samples are not available until a sampling algorithm completely terminates. As testing time is usually limited, we propose an incremental approach of product sampling for pairwise interaction testing (called IncLing), which enables developers to generate samples on demand in a step-wise manner. Furthermore, IncLing uses heuristics to efficiently achieve pairwise interaction coverage with a reasonable number of products. We evaluated IncLing by comparing it against existing sampling algorithms using feature models of different sizes. The results of our approach indicate efficiency improvements for product-line testing.

Design flaws in object-oriented programs may seriously corrupt code quality thus increasing the risk for introducing subtle errors during software maintenance and evolution. Most recent approaches identify design flaws in an ad-hoc manner, either focusing on software metrics, locally restricted code smells, or on coarse-grained architectural anti-patterns. In this paper, we utilize an abstract program model capturing high-level object-oriented code entities, further augmented with qualitative and quantitative design-related information such as coupling/cohesion. Based on this model, we propose a comprehensive methodology for specifying object-oriented design flaws by means of compound rules integrating code metrics, code smells and anti-patterns in a modular way. This approach allows for efficient, automated design-flaw detection through incremental multi-pattern matching, by facilitating systematic information reuse among multiple detection rules as well as between subsequent detection runs on continuously evolving programs. Our tool implementation comprises well-known anti-patterns for Java programs. The results of our experimental evaluation show high detection precision, scalability to real-size programs, as well as a remarkable gain in efficiency due to information reuse.

Testing every member of a product line individually is often impracticable due to large number of possible product configurations. Thus, feature models are frequently used to generate samples, i.e., subsets of product configurations under test. Besides the extensively studied combinatorial interaction testing (CIT) approach for coverage-driven sample generation, only few approaches exist so far adopting mutation testing to emulate faults in feature models to be detected by a sample. In this paper, we present a mutation-based sampling framework for fault-based product-line testing. We define a comprehensive catalog of atomic mutation operators on the graphical representation of feature models. This way, we are able (1) to also define complex mutation operators emulating more subtle faults, and (2) to classify operators semantically, e.g., to avoid redundant and equivalent mutants. We further introduce similarity-based mutant selection and higher order mutation strategies to reduce testing efforts. Our implementation is based on the graph transformation engine Henshin and is evaluated concerning effectiveness/efficiency trade-offs.

The design of an adequate test suite is usually guided by identifying test requirements which should be satisfied by the selected set of test cases. To reduce testing costs, test suite minimization heuristics aim at eliminating redundancy from existing test suites. However, recent test suite minimization approaches lack (1) to handle test suites commonly derived for families of similar software variants under test, and (2) to incorporate fine-grained information concerning cost/profit goals for test case selection. In this paper, we propose a formal framework to optimize test suites designed for sets of software variants under test w.r.t. multiple conflicting cost/profit objectives. The problem representation is independent of the concrete testing methodology. We apply integer linear programming (ILP) to approximate optimal solutions. We further develop an efficient incremental heuristic for deriving a sequence of representative software variants to be tested for approaching optimal profits under reduced costs. We evaluated the algorithm by comparing its outcome to the optimal solution.

Exhaustively testing every product of a software product line (SPL) is a difficult task due to the combinatorial explosion of the number of products. Combinatorial interaction testing is a technique to reduce the number of products under test. However, it is typically up-to the tester in which order these products are tested. We propose a similarity-based prioritization to be applied on these products before they are generated. The proposed approach does not guarantee to find more errors than sampling approaches, but it aims at increasing interaction coverage of an SPL under test as fast as possible over time. This is especially beneficial since usually the time budget for testing is limited. We implemented similarity-based prioritization in FeatureIDE and evaluated it by comparing its outcome to the default outcome of three sampling algorithms as well as to random orders. The experiment results indicate that the order with similarity-based prioritization is better than random orders and often better than the default order of existing sampling algorithms.

Modern software systems are highly configurable in order to satisfy diverse customer requirements and application contexts. Feature models provide a well-established formalism for tailoring configuration spaces of applications. Thereupon, multi-view staged configuration approaches modularize feature models for separation of concerns and apply workflow modeling for scheduling configuration decisions. However, the complex, often oblivious and even cyclic logical dependencies among configuration decisions obstruct compositional semantics of feature model views thus spoiling intuitive modeling and rigorous analysis of staged configuration processes. In this paper, we apply workflow Petri nets (WPNs) as a formal operational model for staged configuration that makes explicit causal dependencies among feature selections. For the internal separation into composable configuration stages we further adopt the principles of open workflow nets. It is shown that the soundness notion of WPNs naturally coincides with fundamental correctness and liveness properties to be verified for staged configuration processes. We present a prototype implementation for an automated computation of staged configuration processes and provide experimental results concerning scalability properties.

Mobile devices like smartphones are getting increasingly important in our daily lifes. They are used in various environments and have to dynamically adapt themselves accordingly in order to provide an optimal runtime behavior. Naturally, adapting to continuously changing environmental conditions is a challenging task because mobile devices are always limited in their resources and have to adapt in real-time. In this paper, we introduce an approach that enables resource limited devices to adapt to changing conditions using dynamic software product lines techniques. Therefore, feature models are reduced to a specific hardware context before installing the adaptive mobile application on the device. This reduces the amount of possible configurations that are compatible with the device and, thereby, minimizes the costs and the duration of an adaptation during runtime.

Cloud-based applications are multi-tenant aware, whereas customers (i.e., tenants) share hardware and software resources. Offering highly configurable applications to thousands of tenants in a shared cloud environment demands for scalable configuration management. Based on an example scenario taken from the Indenica project, we identify requirements for applying methods from software product line (SPL) engineering to configure cloud-based multi-tenant aware applications. Using an extended feature model (EFM) to express variability of functionality and service qualities, we propose a concept for dynamic configuration management to address the identified requirements. Our proposed configuration management includes an adaptive staged configuration process that is capable of adding and removing stakeholders dynamically and that allows for reconfiguration of variants as stakeholders' objectives change.

A seamless model-based methodology for requirements specification becomes increasingly the key to successful software systems engineering. The enhanced activity diagrams of UML 2 offer a promising intuitive modeling approach for requirements capturing. On this basis, we propose a formal syntax and operational semantics and extend activity diagrams to LADs (Live Activity Diagrams) by liveness-enriched constructs inspired by LSCs (Live Sequence Charts) for stating precise execution modalities. We aim at a tool-supported execution of LAD specifications allowing for early simulation and validation of requirements. We present an implementation of an LAD execution engine and describe the there upon suggested requirements engineering approach by means of an automotive case study.

Errors, inconsistences, incompletenesses and ambiguities in the requirements specification are major reasons for the failure of IT projects. Since the new major version 2 of the UML, the suitability of activity diagrams for modeling requirements has increased significantly. UML 2 activity diagrams are based upon a completely reengineered metamodel including many new features and an improved semantic precision. We provide a formal syntax and operational semantics for activity diagrams to allow for fully executable models. Inspired by the scenario-based language of live sequence charts, some extensions for activity diagrams are proposed including a distinction between possible and mandatory behavior. The proposed semantics paves the way for formal reasoning and tool development that allows for early prototyping and validation by simulation.