Specification and automated validation of staged reconfiguration processes for dynamic software product lines

Dynamic software product lines (DSPLs) propose elaborated design and implementation principles for engineering highly configurable runtime-adaptive systems in a sustainable and feature-oriented way. For this, DSPLs add to classical software product lines (SPL) the notions of (1) staged (pre-)configurations with dedicated binding times for each individual feature, and (2) continuous runtime reconfigurations of dynamic features throughout the entire product life cycle. Especially in the context of safety- and mission-critical systems, the design of reliable DSPLs requires capabilities for accurately specifying and validating arbitrary complex constraints among configuration parameters and/or respective reconfiguration options. Compared to classical SPL domain analysis which is usually based on Boolean constraint solving, DSPL validation, therefore, further requires capabilities for checking temporal properties of reconfiguration processes. In this article, we present a comprehensive approach for modeling and automatically verifying essential validity properties of staged reconfiguration processes with complex binding time constraints during DSPL domain engineering. The novel modeling concepts introduced are motivated by (re-)configuration constraints apparent in a real-world industrial case study from the automation engineering domain, which are not properly expressible and analyzable using state-of-the-art SPL domain modeling approaches. We present a prototypical tool implementation based on the model checker SPIN and present evaluation results obtained from our industrial case study, demonstrating the applicability of the approach.     

Model-based pairwise testing for feature interaction coverage in software product line engineering

Testing software product lines (SPLs) is very challenging due to a high degree of variability leading to an enormous number of possible products. The vast majority of today??s testing approaches for SPLs validate products individually using different kinds of reuse techniques for testing. Because of their reusability and adaptability capabilities, model-based approaches are suitable to describe variability and are therefore frequently used for implementation and testing purposes of SPLs. Due to the enormous number of possible products, individual product testing becomes more and more infeasible. Pairwise testing offers one possibility to test a subset of all possible products. However, according to the best of our knowledge, there is no contribution discussing and rating this approach in the SPL context. In this contribution, we provide a mapping between feature models describing the common and variable parts of an SPL and a reusable test model in the form of statecharts. Thereby, we interrelate feature model-based coverage criteria and test model-based coverage criteria such as control and data flow coverage and are therefore able to discuss the potentials and limitations of pairwise testing. We pay particular attention to test requirements for feature interactions constituting a major challenge in SPL engineering. We give a concise definition of feature dependencies and feature interactions from a testing point of view, and we discuss adequacy criteria for SPL coverage under pairwise feature interaction testing and give a generalization to the T-wise case. The concept and implementation of our approach are evaluated by means of a case study from the automotive domain.     

CPA/Tiger-MGP: test-goal set partitioning for efficient multi-goal test-suite generation

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 CPA checker.

     

Effective product-line testing using similarity-based product prioritization

Software and Systems Modeling - A software product line comprises a family of software products that share a common set of features. Testing an entire product-line product-by-product is infeasible...     

Reasoning about product-line evolution using complex feature model differences

Features define common and variable parts of the members of a (software) product line. Feature models are used to specify the set of all valid feature combinations. Feature models not only enjoy an intuitive tree-like graphical syntax, but also a precise formal semantics, which can be denoted as propositional formulae over Boolean feature variables. A product line usually constitutes a long-term investment and, therefore, has to undergo continuous evolution to meet ever-changing requirements. First of all, product-line evolution leads to changes of the feature model due to its central role in the product-line paradigm. As a result, product-line engineers are often faced with the problems that (1) feature models are changed in an ad-hoc manner without proper documentation, and (2) the semantic impact of feature diagram changes is unclear. In this article, we propose a comprehensive approach to tackle both challenges. For (1), our approach compares the old and new version of the diagram representation of a feature model and specifies the changes using complex edit operations on feature diagrams. In this way, feature model changes are automatically detected and formally documented. For (2), we propose an approach for reasoning about the semantic impact of diagram changes. We present a set of edit operations on feature diagrams, where complex operations are primarily derived from evolution scenarios observed in a real-world case study, i.e., a product line from the automation engineering domain. We evaluated our approach to demonstrate its applicability with respect to the case study, as well as its scalability concerning experimental data sets.     

ARDEN2BYTECODE: a one-pass Arden Syntax compiler for service-oriented decision support systems based on the OSGi platform

Patient empowerment might be one key to reduce the pressure on health care systems challenged by the expected demographic changes. Knowledge based systems can, in combination with automated sensor measurements, improve the patients' ability to review their state of health and make informed decisions. The Arden Syntax as a standardized language to represent medical knowledge can be used to express the corresponding decision rules. In this paper we introduce ARDEN2BYTECODE, a newly developed open source compiler for the Arden Syntax. ARDEN2BYTECODE runs on Java Virtual Machines (JVM) and translates Arden Syntax directly to Java Bytecode (JBC) executable on JVMs. ARDEN2BYTECODE easily integrates into service oriented architectures, like the Open Services Gateway Initiative (OSGi) platform. Apart from an evaluation of compilation performance and execution times, ARDEN2BYTECODE was integrated into an existing knowledge supported exercise training system and recorded training sessions have been used to check the implementation.