The variability of product lines can exceed purely Boolean configuration spaces. Cardinality-based Feature Models (CFMs) are employed to model multi-instantiation of features along with individually configurable subtrees. Due to the added complexity, the analysis of CFMs cannot be done with state-of-the-art, SAT-based tooling for analyzing Boolean Feature Models (FMs). Analyses on FMs include checking for satisfying configurations, dead features, false optional features, and whether specific configurations are valid according to the FM. In this work, we compare different solver encodings to enable analysis for CFMs. First, we generalize the analyses on Boolean FMs to the notion of cardinalities and the new anomalies that can occur. Second, we present three different mathematical encodings of CFMs for automated reasoning using solvers. Third, we implement the encoding for ILP, SMT, and CSP solvers. We evaluate the feasibility and performance of our encodings on current ILP, SMT, and CSP solvers. Our evaluation shows that our encoding for CSP solvers enables all common analyses with the best performance among the compared encodings and solvers.

Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC) : an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.

Information and communication technology (ICT) offers promising opportunities to address global sustainability challenges such as climate change and social inequality by enabling energy savings and social innovations. At the same time, ICT threatens to exacerbate these crises, as evident in the increasing consumption of resources and widening digital inequalities. As one of the enablers of ICT, software engineering plays a key role to tackle the problems and explore the potentials of ICT for sustainability. However, sustainability in software engineering is still a niche topic, with little structure, a limited understanding of sustainability and few comprehensive strategies. In this article, we introduce the main concepts of Sustainable Software Engineering, critically review the state of research and identify seven future research challenges across all research areas. We further present our research vision—sustainability-driven software engineering and transdisciplinary research formats—and outline a research roadmap with the key steps to be achieved by 2030.

Feature models are commonly used to specify valid configurations of a product line. In industry, feature models are often complex due to numerous 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. Even worse, most counting-based analyses require evaluation for multiple features or partial configurations resulting in numerous # SAT computations on the same feature model. Instead of 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 repetitive counting queries on features and partial configurations. In our experiments, reusing d-DNNFs saved up-to \(\sim\) 99.98% compared to repetitive invocations of # SAT solvers even when including compilation times. Overall, our tool ddnnife combined with the d-DNNF compiler d4 appears to be the most promising option when dealing with many repetitive feature-model counting queries.

Abstract Product lines are widely used to manage families of products that share a common base of features. Typically, not every combination (configuration) of features is valid. Feature models are a de facto standard to specify valid configurations and allow standardized analyses on the variability of the underlying system. A large variety of such analyses depends on computing the number of valid configurations. To analyze feature models, they are typically translated to propositional logic. This allows to employ SAT solvers that compute the number of satisfying assignments of the propositional formula translated from a feature model. However, the SAT problem is generally assumed to be even harder than SAT and its scalability when applied to feature models has only been explored sparsely. Our main contribution is an investigation of the performance of off-the-shelf SAT solvers on computing the number of valid configurations for industrial feature models. We empirically evaluate 21 publicly available SAT solvers on 130 feature models from 15 subject systems. Our results indicate that current solvers master a majority of the evaluated systems (13/15) with the fastest solvers requiring less than one second for each successfully evaluated feature model. However, there are two complex systems for which none of the evaluated solvers scales. For the given experiment design, the solvers that consumed the least runtime are (2.5 seconds in sum for the 13 systems) and (3.5 seconds).

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.

Security-critical software applications contain confidential information which has to be protected from leaking to unauthorized systems. With language-based techniques, the confidentiality of applications can be enforced. Such techniques are for example type systems that enforce an information flow policy through typing rules. The precision of such type systems, especially in object-oriented languages, is an area of active research: an appropriate system should not reject too many secure programs while soundly preserving noninterference. In this work, we introduce the language SIFO which supports information flow control for an object-oriented language with type modifiers. Type modifiers increase the precision of the type system by utilizing immutability and uniqueness properties of objects for the detection of information leaks. We present SIFO informally by using examples to demonstrate the applicability of the language, formalize the type system, prove noninterference, implement SIFO as a pluggable type system in the programming language L42, and evaluate it with a feasibility study and a benchmark.

Validating a configurable software system is challenging, as there are potentially millions of configurations, which makes testing each configuration individually infeasible. Thus, existing sampling algorithms allow to compute a representative subset of configurations, called sample, that can be tested instead. However, sampling on the set of configurations may miss potential error sources on implementation level. In this paper, we present solution-space sampling, a concept that mitigates this problem by allowing to sample directly on the implementation level. We apply solution-space sampling to six real-word, automotive product lines and show that it produces up to 56 % smaller samples, while also covering all potential error sources missed by problem-space sampling.

A software product line allows to derive individual software products based on a configuration. As the number of configurations is an indicator for the general complexity of a software product line, automatic #SAT analyses have been proposed to provide this information. However, the number of configurations does not need to match the number of derivable products. Due to this mismatch, using the number of configurations to reason about the software complexity (i.e., the number of derivable products) of a software product line can lead to wrong assumptions during implementation and testing. How to compute the actual number of derivable products, however, is unknown. In this paper, we mitigate this problem and present a concept to derive a solution-space feature model which allows to reuse existing #SAT analyses for computing the number of derivable products of a software product line. We apply our concept to a total of 119 subsystems of three industrial software product lines. The results show that the derivation scales for real world software product lines and confirm the mismatch between the number of configurations and the number of products.

Abstract A product line is an approach for systematically managing configuration options of customizable systems, usually by means of features. Products are generated for configurations consisting of selected features. Product-line evolution can lead to unintended changes to product behavior. We illustrate that updating configurations after product-line evolution requires decisions of both, domain engineers responsible for product-line evolution as well as application engineers responsible for configurations. The challenge is that domain and application engineers might not be able to interact with each other. We propose a formal foundation and a methodology that enables domain engineers to guide application engineers through configuration evolution by sharing knowledge on product-line evolution and by defining automatic update operations for configurations. As an effect, we enable knowledge transfer between those engineers without the need for interactions. We evaluate our methodology on four large-scale industrial product lines. The results of the qualitative evaluation indicate that our method is flexible enough for real-world product-line evolution. The quantitative evaluation indicates that we detect product behavior changes for up to $$55.3\%$$ 55.3 % of the configurations which would not have been detected using existing methods.

Cyber-physical systems are ubiquitous nowadays. However, as automation increases, modeling and verifying them becomes increasingly difficult due to the inherently complex physical environment. Skill graphs are a means to model complex cyber-physical systems (e.g., vehicle automation systems) by distributing complex behaviors among skills with interfaces between them. We identified that skill graphs have a high potential to be amenable to scalable verification approaches in the early software development process. In this work, we suggest combining skill graphs with hybrid programs. Hybrid programs constitute a program notation for hybrid systems enabling the verification of cyber-physical systems. We provide the first formalization of skill graphs including a notion of compositionality and propose Skeditor , an integrated framework for modeling and verifying them. Skeditor is coupled with the theorem prover KeYmaera X , which is specialized in the verification of hybrid programs. In an experiment exhibiting the follow mode of a vehicle, we evaluate our skill-based methodology with respect to savings in verification effort and potential to find modeling defects at design time. Compared to non-compositional verification, the initial verification effort needed is reduced by more than 53%.

Software product lines are increasingly used to handle the growing demand of custom-tailored software variants. They provide systematic reuse of software paired with variability mechanisms in the code to implement whole product families rather than single software products. A common domain of application for product lines are safety-critical systems, which require behavioral correctness to avoid dangerous situations in-field. While most approaches concentrate on post-hoc verification for product lines, we argue that a stepwise approach to create correct programs may be beneficial for developers to manage the growing variability. Correctness-by-construction is such a stepwise approach to create programs using a set of small, tractable refinement rules that guarantee the correctness of the program with regard to its specification. In this paper, we propose the first approach to develop correct-by-construction software product lines using feature-oriented programming. First, we extend correctness-by-construction by two refinement rules for variation points in the code. Second, we give a proof for the soundness of the proposed rules. Third, we implement our technique in a tool called VarCorC and show the applicability of the tool by conducting two case studies.

Automated production systems (aPS) are variant-rich, design-to-order systems and an increasing proportion of their functionality is implemented by control software. In control software development, software reuse is still commonly performed via clone-and-own despite many drawbacks, e.g., copying errors. This unplanned reuse leads to a high amount of historically grown software variants, which contain valuable domain expertise. Therefore, to enable planned reuse of existing control software solutions, an analysis of legacy software, inducing documentation of identified variability, is required. While so-called Software Product Lines enable the documentation of variability, they lack suitable variability visualization tailored to the needs of aPS stakeholders such as application or module developers. To address this gap, this paper introduces a variability visualization concept tailored to the needs of aPS stakeholders with the aim of supporting them in their daily tasks. The concept was evaluated successfully within a master student's course by use of a prototypical implementation of the visualization concept.

Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification. Although CbC is supposed to lead to code with a low defect rate, it is not prevalent, especially because appropriate tool support is missing. To promote CbC, we provide tool support for CbC-based program development. We present CorC, a graphical and textual IDE to create programs in a simple while-language following the CbC approach. Starting with a specification, our open source tool supports CbC developers in refining a program by a sequence of refinement steps and in verifying the correctness of these refinement steps using the theorem prover KeY. We evaluated the tool with a set of standard examples on CbC where we reveal errors in the provided specification. The evaluation shows that our tool reduces the verification time in comparison to post-hoc verification.

Industrial automated production systems are mechatronic and long living systems that undergo changing requirements throughout their life cycle. While the proportion of functionality implemented by software is growing, adjustments are usually implemented using a clone-and-own principle, which results in unmanaged software variants and versions. Furthermore, the need for adapting the control software also results from changes in other disciplines such as mechanical or electrical/electronics. The various drawbacks on software maintainability, that are provoked through clone-andown, call for a shift to modular development. As a first step to realize this migration, software projects need to be analyzed in terms of variability. Secondly, visualization patterns reflecting variability are needed to present the analysis results to domain experts. However, choosing an appropriate visualization is challenging as different domain experts pursue different aims, which should be supported by the visualization and might even require different levels of detail. In this paper, visualization patterns for three different use scenarios are proposed and evaluated using an apprentice group and industrial expert feedback.

Software product line engineering (SPLE) provides a systematic approach to manage variants and versions arising throughout the development of software systems. While SPLE is successfully applied for variant management in the domain of software engineering, the approach is still not widely spread in industrial automated production systems (aPS). Previous studies highlight the interdisciplinary nature of aPS as a reason for not applying SPLE, since control software variants and versions also result from changes in other disciplines such as the mechanical engineering department (i.e. exchange of a sensor). Additionally, the software may evolve over decades at the customer site. In order to gain a better understanding of the challenges in the development of aPS and the constraints hindering the use of SPLE, we conducted several interviews with software development engineers from the domain of aPS. The interviews main aim was to get an overview of the current state of variability management and applied planned and unplanned software reuse strategies. Based on these insights, we summarize the main results useable for a transition from currently deployed variability management concepts in aPS to the SPLE approach.

Model-based languages such as MATLAB/Simulink are crucial for the development of embedded software systems. To adapt to changing requirements, engineers commonly copy and modify existing systems to create new variants. Commonly referred to as clone-and-own, this reuse strategy is easy to apply and beneficial in the short term, but it entails severe maintenance and consistency issues in the long term, leading to a huge amount of redundant and similar assets. Moreover, a later transition towards structured reuse such as with software product lines inevitably requires the comparison of all existing variants prior to the actual migration. However, current work mostly revolves around the comparison of only two systems and despite approaches proposed that can cope with more, such are not applicable to embedded software systems such as MATLAB/Simulink. In this paper, we bridge this gap and propose Static Connectivity Matrix Analysis (SCMA), a novel comparison procedure that allows for the evaluation of multiple MATLAB/Simulink model variants at once. In particular, we transform models into a matrix form which is used to compare all models and to identify all similar structures between them, even with model parts being completely relocated during clone-and-own. We allow engineers to tailor results and to focus on any arbitrary variant subset, enabling individual reasoning prior to migration. We provide a feasibility study from the automotive domain, showing our matrix representation to be suitable and our technique to be fast and precise.

A Software Product Line (SPL) is an approach to reuse in-the-large that models closely related software systems in terms of commonalities and variabilities. Design patterns are best practices for addressing recurring design problems. When implementing an SPL, instances of certain design patterns are employed to handle variability, which makes these variability-aware design patterns a best practice for SPL design. However, a proactive SPL development method with design patterns is lacking. In our paper [1], we present a method to perform generative SPL development with design patterns.

The analysis of software product lines is challenging due to the potentially large number of products, which grow exponentially in terms of the number of features. Product sampling is a technique used to avoid exhaustive testing, which is often infeasible. In this paper, we propose a classification for product sampling techniques and classify the existing literature accordingly. We distinguish the important characteristics of such approaches based on the information used for sampling, the kind of algorithm, and the achieved coverage criteria. Furthermore, we give an overview on existing tools and evaluations of product sampling techniques. We share our insights on the state-of-the-art of product sampling and discuss potential future work.

Testing is a fundamental task to ensure software quality. Regression testing aims to ensure that changes to software do not introduce new failures. As resources are often limited and testing comprises a vast amount of test cases, different regression strategies have been proposed to reduce testing effort by selecting or prioritizing important test cases, e.g., code coverage (to ensure a sufficient testing depth). However, in system testing, source code is often not available creating a black-box system. In this paper, we introduce an automated, multi-objective test case selection technique in black-box systems using genetic algorithms. We define seven different objectives, based on meta-data, allowing a flexible test case selection for a variety of systems. For evaluation, we apply our technique on two different subject systems assessing the feasibility and suitability of our test case selection approach. Results indicate that our approach is applicable based on different data available and is able to outperform random test case selection and retest-all.

Feature modeling has emerged as the de-facto standard to compactly capture the variability of a software product line. Multiple feature modeling languages have been proposed that evolved over the last decades to manage industrial-size product lines. However, less expressive languages, solely permitting require and exclude constraints, are permanently and carelessly used in product-line research. We address the problem whether those less expressive languages are sufficient for industrial product lines. We developed an algorithm to eliminate complex cross-tree constraints in a feature model, enabling the combination of tools and algorithms working with different feature model dialects in a plug-and-play manner. However, the scope of our algorithm is limited. Our evaluation on large feature models, including the Linux kernel, gives evidence that require and exclude constraints are not sufficient to express real-world feature models. Hence, we promote that research on feature models needs to consider arbitrary propositional formulas as cross-tree constraints prospectively.

Regression testing is the common task of retesting software that has been changed or extended (e.g., by new features) during software evolution. As retesting the whole program is not feasible with reasonable time and cost, usually only a subset of all test cases is executed for regression testing, e.g., by executing test cases according to test case prioritization. Although a vast amount of methods for test case prioritization exist, they mostly require access to source code (i.e., white-box). However, in industrial practice, system-level testing is an important task that usually grants no access to source code (i.e., black-box). Hence, for an effective regression testing process, other information has to be employed. In this paper, we introduce a novel technique for test case prioritization for manual system-level regression testing based on supervised machine learning. Our approach considers black-box meta-data, such as test case history, as well as natural language test case descriptions for prioritization. We use the machine learning algorithm SVM Rank to evaluate our approach by means of two subject systems and measure the prioritization quality. Our results imply that our technique improves the failure detection rate significantly compared to a random order. In addition, we are able to outperform a test case order given by a test expert. Moreover, using natural language descriptions improves the failure finding rate.

Developing and managing software variants is a key challenge in today's software development. Due to conflicting requirements, software is developed in multiple variants to satisfy the needs of individual customers. While software product lines allow the efficient development of a high number of variants, many projects in industrial software development start with few variants, where each variant is developed separately. Unfortunately, for an increasing number of variants, this clone-and-own approach becomes error-prone and unprofitable regarding synchronization of changes between variants. With VariantSync, we demonstrate a tool to reduce the gap between clone-and-own and product lines by automating the synchronization of software variants and simplifying a potential later transition to a product line.

Block-based modeling languages, such as MATLAB/Simulink or state charts, reduce the complexity inherent to developing large-scale software systems. When creating variants for largely similar yet different software systems, the common practice is to copy models and modify them to different requirements. While this allows companies to save costs in the short-term, these so-called clone-and-own approaches cause problems regarding long-term evolution and system quality as the relation between the variants of the resulting software family is lost so that the variants have to be maintained in isolation. To recreate information regarding the variants' relations, variability mining identifies common and varying parts of cloned variants but, currently, the respective algorithms have to be created for each target language individually. In this paper, we present a generalized method to instantiate variability mining for arbitrary block-based modeling languages. The identified variability information allows developers to understand the variability of their grown software family. This knowledge helps efficiently maintaining the variants and allows migrating from clone-and-own approaches to more elaborate reuse strategies, such as software product lines. We demonstrate the feasibility of our method by instantiating variability mining techniques for two block-based languages.

Software Product Lines (SPLs) are an approach to reuse in-the-large that models a set of closely related software systems in terms of commonalities and variabilities. Design patterns are best practices for addressing recurring design problems in object-oriented source code. In the practice of implementing an SPL, instances of certain design patterns are employed to handle variability, which makes these "variability-aware design patterns" a best practice for SPL design. However, there currently is no dedicated method for proactively developing SPL using design patterns suitable for realizing variable functionality. In this paper, we present a method to perform generative SPL development with design patterns. We use role models to capture design patterns and their relation to a variability model. We further allow mapping of individual design pattern roles to elements of realization artifacts to be generated (e.g., classes, methods) and check the conformance of the realization with the specification of the pattern. With this method, we support proactive development of SPL using design patterns to apply best practices for the realization of variability. We present an implementation of our approach within the Eclipse IDE and demonstrate it within a case study.

Automated machines and plants are operated for some decades and undergo an everlasting evolution during this time. In this paper, we present three related open evolution challenges focusing on software evolution in the domain of automated production systems, i.e. evolution and co-evolution of (interdisciplinary) engineering models and code, quality assurance as well as variant and version management during evolution.

Automated production systems involve multiple engineering disciplines and often operate for several decades. Therefore, in order to leverage benefits of model-based system engineering, modeling approaches must handle both multiple disciplines and variability. As a first step towards variability modeling and management, a small case study is carried out to investigate the opportunities and challenges when enhancing an interdisciplinary modeling approach with delta modeling - a technique for specifying variants and versions. The paper reflects critically its applicability, implications as well as potential beneficial impacts and discusses encouraging challenges and next steps towards an interdisciplinary approach for variability modeling and management.

In software performance engineering, what-if scenarios, architecture optimization, capacity planning, run-time adaptation, and uncertainty management of realistic models typically require the evaluation of many instances. Effective analysis is however hindered by two orthogonal sources of complexity. The first is the infamous problem of state space explosion -- the analysis of a single model becomes intractable with its size. The second is due to massive parameter spaces to be explored, but such that computations cannot be reused across model instances. In this paper, we efficiently analyze many queuing models with the distinctive feature of more accurately capturing variability and uncertainty of execution rates by incorporating general (i.e., non-exponential) distributions. Applying product-line engineering methods, we consider a family of models generated by a core that evolves into concrete instances by applying simple delta operations affecting both the topology and the model's parameters. State explosion is tackled by turning to a scalable approximation based on ordinary differential equations. The entire model space is analyzed in a family-based fashion, i.e., at once using an efficient symbolic solution of a super-model that subsumes every concrete instance. Extensive numerical tests show that this is orders of magnitude faster than a naive instance-by-instance analysis.

To support users in operating a computer system with a varying set of functions, it is fundamental to understand their intentions, e.g., within an in-car infotainment system. Although the development of current in-car infotainment systems is already model-based, explicitly gathering and modeling user intentions is currently not supported. However, manually creating software that predicts user intentions is complex, error-prone and expensive. Model-based development can help in overcoming these issues. In this paper, we present an approach for modeling a user's intention based on Bayesian networks. We support developers of in-car infotainment systems by providing means to model possible intentions of users according to the current situation. We further allow modeling of user preferences and show how the modeled intentions may change during run-time as a result of the user's behavior. We demonstrate feasibility of our approach using an industrial example of an intention-aware in-car infotainment system.

Software product lines have potential to allow for mass customization of products. Unfortunately, the resulting, vast amount of possible product variants with commonalities and differences leads to new challenges in software testing. Ideally, every product variant should be tested, especially in safety-critical systems. However, due to the exponentially increasing number of product variants, testing every product variant is not feasible. Thus, new concepts and techniques are required to provide efficient SPL testing strategies exploiting the commonalities of software artifacts between product variants to reduce redundancy in testing. In this paper, we present an efficient integration testing approach for SPLs based on delta modeling. We focus on test case prioritization. As a result, only the most important test cases for every product variant are tested, reducing the number of executed test cases significantly, as testing can stop at any given point because of resource constraints while ensuring that the most important test cases have been covered. We present the general concept and our evaluation results. The results show a measurable reduction of executed test cases compared to single-software testing approaches.

The analysis of nowadays software systems for supporting, e.g., testing, verification or debugging is becoming more challenging due to their increasing complexity. Model slicing is a promising analysis technique to tackle this issue by abstracting from those parts not influencing the current point of interest. In the context of software product lines, applying model slicing separately for each variant is in general infeasible. Delta modeling allows exploiting the explicit specification of commonality and variability within deltas and enables the reuse of artifacts and already obtained results to reduce the modeling and analysis efforts. In this paper, we propose a novel approach for incremental model slicing for delta-oriented software product lines. Based on the specification of model changes between variants by means of model regression deltas, an incremental adaptation of variant-specific dependency graphs as well as an incremental slice computation is achieved. The slice computation further allows for the derivation of differences between slices for the same point of interest enhancing, e.g., change impact analysis. We provide details of our incremental approach, discuss benefits and present future work.

Coping with evolution in automated production systems implies a cross-disciplinary challenge along the system's life-cycle for variant-rich systems of high complexity. The authors from computer science and automation provide an interdisciplinary survey on challenges and state of the art in evolution of automated production systems. Selected challenges are illustrated on the case of a simple pick and place unit. In the first part of the paper, we discuss the development process of automated production systems as well as the different type of evolutions during the system's life-cycle on the case of a pick and place unit. In the second part, we survey the challenges associated with evolution in the different development phases and a couple of cross-cutting areas and review existing approaches addressing the challenges. We close with summarizing future research directions to address the challenges of evolution in automated production systems.

Delta modelling is an approach to facilitate the automated product derivation for software product lines. It is based on a set of deltas specifying modifications that are incrementally applied to a core product. The applicability of deltas depends on application conditions over features. This paper presentsabstract delta modelling, which explores delta modelling from an abstract, algebraic perspective. Compared to the previous work, we take a more flexible approach to conflicts between modifications by introducing the notion of conflict-resolving deltas. Furthermore, we extend our approach to allow the nesting of delta models for increased modularity. We also present conditions on the structure of deltas to ensure unambiguous product generation.

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.

Modern software systems outgrow the scope of traditional software product lines (SPLs) resulting in multi software product lines (MSPLs) with many interconnected subsystem versions and variants. Delta-oriented programming (DOP) is a flexible, modular approach for implementing SPLs, but DOP so far does not allow the realization of MSPLs. In this paper, we extend DOP to support MSPL development and provide the first holistic modeling approach for MSPLs that spans problem, solution and configuration space. The main concept is the extension of DOP with the possibility to import other SPLs or MSPLs into a new MSPL. By expressing constraints amongst the imported SPLs, a common configuration and product generation is enabled.

Software product lines (SPLs) and software ecosystems (SECOs) encompass a family of closely related software systems in terms of common and variable assets that are configured to concrete products (variability in space). Over the course of time, variable assets of SPLs and especially SECOs are subject to change in order to meet new requirements as part of software evolution (variability in time). Even though both dimensions of variability have to be handled simultaneously, e.g., as not all customers upgrade their respective products immediately or completely, there currently is no approach that can create variants with a selection of variable assets in various versions. In this paper, we introduce an integrated approach to manage variability in space and time in software families using Hyper Feature Models (HFMs) with feature versions and combine them with an extension of the transformational variability realization mechanism delta modeling. This allows derivation of concrete software systems from an SPL or SECO configuring both functionality (features) as well as versions.

Abstract Traits have been proposed as a more flexible mechanism than class inheritance for structuring code in object-oriented programming, to achieve fine-grained code reuse. A trait originally developed for one purpose can be adapted and reused in a completely different context. Formalizations of traits have been extensively studied, and implementations of traits have started to appear in programming languages. So far, work on formally establishing properties of trait-based programs has mostly concentrated on type systems. This paper presents the first deductive proof system for a trait-based object-oriented language. If a specification of a trait can be given a priori, covering all actual usage of that trait, our proof system is modular as each trait is analyzed only once. However, imposing such a restriction may in many cases unnecessarily limit traits as a mechanism for flexible code reuse. In order to reflect the flexible reuse potential of traits, our proof system additionally allows new specifications to be added to a trait in anincrementalway which does not violate established proofs. We formalize and show the soundness of the proof system.

FMSPLE 2013 is the fourth edition of the FMSPLE workshop series aimed at connecting researchers and practitioners interested in raising the efficiency and the effectiveness of software product line engineering through the application of innovative analysis approaches and formal methods.

Delta modeling is a modular, yet flexible approach to capture spatial and temporal variability by explicitly representing the differences between system variants or versions. The conceptual idea of delta modeling is language-independent. But, in order to apply delta modeling for a concrete language, so far, a delta language had to be manually developed on top of the base language leading to a large variety of heterogeneous language concepts. In this paper, we present a process that allows deriving a delta language from the grammar of a given base language. Our approach relies on an automatically generated language extension that can be manually adapted to meet domain-specific needs. We illustrate our approach using delta modeling on a textual variant of statecharts.

Delta-oriented programming (DOP) is a flexible approach for implementing software product lines (SPLs). DOP SPLs are implemented by a code base (a set of delta modules encapsulating changes to object-oriented programs) and a product line declaration (providing the connection of the delta modules with the product features). In this paper, we extend DOP by the capability to switch the implemented product configuration at runtime and present a formal foundation for dynamic DOP. A dynamic DOP SPL is a DOP SPL with a dynamic reconfiguration graph that specifies how to switch between different feature configurations. Dynamic DOP supports (unanticipated) software evolution such that at runtime, the product line declaration, the code base and the dynamic reconfiguration graph can be changed in any (unanticipated) way that preserves the currently running product. The type system of our dynamic DOP core calculus ensures that the dynamic reconfigurations lead to type safe products and do not cause runtime type errors.

A software product line is a set of similar software products that share a common code base. While software product lines can be implemented efficiently using feature-oriented programming, verifying each product individually does not scale, especially if human effort is required (e.g., as in interactive theorem proving). We present a family-based approach of deductive verification to prove the correctness of a software product line efficiently. We illustrate and evaluate our approach for software product lines written in a feature-oriented dialect of Java and specified using the Java Modeling Language. We show that the theorem prover KeY can be used off-the-shelf for this task, without any modifications. Compared to the individual verification of each product, our approach reduces the verification time needed for our case study by more than 85%.

FMSPLE 2012 is the third edition of the FMSPLE workshop series, traditionally affiliated with SPLC, which aims to connect researchers and practitioners interested in raising the efficiency and the effectiveness of SPLE through the application of innovative analysis approaches and formal methods.

Delta-oriented programming is a modular, yet flexible technique to implement software product lines. To efficiently verify the specifications of all possible product variants of a product line, it is usually infeasible to generate all product variants and to verify them individually. To counter this problem, we propose a transformational proof system in which the specifications in a delta module describe changes to previous specifications. Our approach allows each delta module to be verified in isolation, based on symbolic assumptions for calls to methods which may be in other delta modules. When product variants are generated from delta modules, these assumptions are instantiated by the actual guarantees of the methods in the considered product variant and used to derive the specifications of this product variant.

Traits have been proposed as a more flexible mechanism for code structuring in object-oriented programming than class inheritance, for achieving fine-grained code reuse. A trait originally developed for one purpose can be modified and reused in a completely different context. Formalizations of traits have been extensively studied, and implementations of traits have started to appear in programming languages. However, work on formally establishing properties of trait-based programs has so far mostly concentrated on type systems. This paper proposes the first deductive proof system for a trait-based object-oriented language. If a specification for a trait can be given a priori, covering all actual usage of that trait, our proof system is modular as each trait is analyzed only once. In order to reflect the flexible reuse potential of traits, our proof system additionally allows new specifications to be added to a trait in an incremental way which does not violate established proofs. We formalize and show the soundness of the proof system.

Traditional syntax-oriented variability modeling specifies the set of possible system variants by explicitly describing how variability is expressed by linguistic means and it concentrates on the set of features that may or may not be present in a product. In contrast, constraint-based variability modeling defines variability in a top-down way by restricting the set of possible compositions of reusable artifacts in terms of properties and by including in this declarative description also some behavioral knowledge the experts may have about the product. Concretely, we propose here to integrate constraint-based solution space variability modeling with feature-oriented problem space variability modeling. This new approach paves the way to significantly simplify feature-oriented software development of product lines: Each feature is described by a set of constraints capturing what the feature contributes to a product variant and expects from it, and, for a given feature selection, the set of associated feature constraints allows synthesizing the set of product variants satisfying the constraints automatically. We illustrate and evaluate the proposed approach on the concrete example of a family of workflows from the bioinformatics domain.

Hierarchically decomposed component-based system development reduces design complexity by supporting distribution of work and component reuse. For product line development, the variability of the components to be deployed in different products has to be represented by appropriate means. In this paper, we propose hierarchical variability modeling which allows specifying component variability integrated with the component hierarchy and locally to the components. Components can contain variation points determining where components may vary. Associated variants define how this variability can be realized in different component configurations. We present a meta model for hierarchical variability modeling to formalize the conceptual ideas. In order to obtain an implementation of the proposed approach together with tool support, we extend the existing architectural description language MontiArc with hierarchical variability modeling. We illustrate the presented approach using an example from the automotive systems domain.

Delta modeling is an approach to facilitate automated product derivation for software product lines. It is based on a set of deltas specifying modifications that are incrementally applied to a core product. The applicability of deltas depends on feature-dependent conditions. This paper presents abstract delta modeling, which explores delta modeling from an abstract, algebraic perspective.

Adaptation is increasingly used in the development of safety-critical embedded systems, in particular to reduce hardware needs and to increase availability. However, composing a system from many reconfigurable components can lead to a huge number of possible system configurations, inducing a complexity that cannot be handled during system design. To overcome this problem, we propose a new component-based modeling and verification method for adaptive embedded systems. The component-based modeling approach facilitates abstracting a composition of components to a hierarchical component. In the hierarchical component, the number of possible configurations of the composition is reduced to a small number of hierarchical configurations. Only these hierarchical configurations have to be considered when the hierarchical component is used in further compositions such that design complexity is reduced at each hierarchical level. In order to ensure well-definedness of components, we provide a model of computation enabling the formal verification of critical requirements of the adaptation behavior.

Formal verification of adaptive systems allows rigorously proving critical requirements. However, design-level models are in general too complex to be handled by verification tools directly. To counter this problem, we propose to reduce model complexity on design-model level in order to facilitate model-based verification. First, we transfer existing compositional reasoning techniques for foundational models used in verification tools to design-level models. Second, we develop new compositional strategies exploiting the special features of adaptive models. Based on these results, we establish a framework for modular model-based verification of adaptive systems by model checking.