Showing 1–25 of 25 results for author: Schaefer, I

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.

ACM Class: D.2

Towards View-based Development of Quantum Software

Authors: Joshua Ammermann, Wolfgang Mauerer, Ina Schaefer

Abstract: Quantum computing is an interdisciplinary field that relies on the expertise of many different stakeholders. The views of various stakeholders on the subject of quantum computing may differ, thereby complicating communication. To address this, we propose a view-based quantum development approach based on a Single Underlying Model (SUM) and a supporting quantum Integrated Development Environment (I… ▽ More Quantum computing is an interdisciplinary field that relies on the expertise of many different stakeholders. The views of various stakeholders on the subject of quantum computing may differ, thereby complicating communication. To address this, we propose a view-based quantum development approach based on a Single Underlying Model (SUM) and a supporting quantum Integrated Development Environment (IDE). We highlight emerging challenges for future research. △ Less

Submitted 26 June, 2024; originally announced June 2024.

Comments: 5 pages, 2 figures, accepted at GI QC Workshop 2024 and to be published in the GI conference proceedings, this is a preprint version before submission

SOTIF-Compliant Scenario Generation Using Semi-Concrete Scenarios and Parameter Sampling

Authors: Lukas Birkemeyer, Julian Fuchs, Alessio Gambi, Ina Schaefer

Abstract: The SOTIF standard (ISO 21448) requires scenario-based testing to verify and validate Advanced Driver Assistance Systems and Automated Driving Systems but does not suggest any practical way to do so effectively and efficiently. Existing scenario generation approaches either focus on exploring or exploiting the scenario space. This generally leads to test suites that cover many known cases but pote… ▽ More The SOTIF standard (ISO 21448) requires scenario-based testing to verify and validate Advanced Driver Assistance Systems and Automated Driving Systems but does not suggest any practical way to do so effectively and efficiently. Existing scenario generation approaches either focus on exploring or exploiting the scenario space. This generally leads to test suites that cover many known cases but potentially miss edge cases or focused test suites that are effective but also contain less diverse scenarios. To generate SOTIF-compliant test suites that achieve higher coverage and find more faults, this paper proposes semi-concrete scenarios and combines them with parameter sampling to adequately balance scenario space exploration and exploitation. Semi-concrete scenarios enable combinatorial scenario generation techniques that systematically explore the scenario space, while parameter sampling allows for the exploitation of continuous parameters. Our experimental results show that the proposed concept can generate more effective test suites than state-of-the-art coverage-based sampling. Moreover, our results show that including a feedback mechanism to drive parameter sampling further increases test suites' effectiveness. △ Less

Submitted 14 August, 2023; originally announced August 2023.

Comments: accepted at IEEE ITSC 2023

Is Scenario Generation Ready for SOTIF? A Systematic Literature Review

Authors: Lukas Birkemeyer, Christian King, Ina Schaefer

Abstract: Scenario-based testing is considered state-of-the-art to verify and validate Advanced Driver Assistance Systems or Automated Driving Systems. Due to the official launch of the SOTIF-standard (ISO 21448), scenario-based testing becomes more and more relevant for releasing those Highly Automated Driving Systems. However, an essential missing detail prevent the practical application of the SOTIF-stan… ▽ More Scenario-based testing is considered state-of-the-art to verify and validate Advanced Driver Assistance Systems or Automated Driving Systems. Due to the official launch of the SOTIF-standard (ISO 21448), scenario-based testing becomes more and more relevant for releasing those Highly Automated Driving Systems. However, an essential missing detail prevent the practical application of the SOTIF-standard: How to practically generate scenarios for scenario-based testing? In this paper, we perform a Systematic Literature Review to identify techniques that generate scenarios complying with requirements of the SOTIF-standard. We classify existing scenario generation techniques and evaluate the characteristics of generated scenarios wrt. SOTIF requirements. We investigate which details of the real-world are covered by generated scenarios, whether scenarios are specific for a system under test or generic, and whether scenarios are designed to minimize the set of unknown and hazardous scenarios. We conclude that scenarios generated with existing techniques do not comply with requirements implied by the SOTIF-standard; hence, we propose directions for future research. △ Less

Submitted 8 August, 2023; v1 submitted 4 August, 2023; originally announced August 2023.

Comments: accepted at IEEE ITSC 2023

QbC: Quantum Correctness by Construction

Authors: Anurudh Peduri, Ina Schaefer, Michael Walter

Abstract: 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 correctne… ▽ More 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. △ Less

Submitted 5 February, 2024; v1 submitted 28 July, 2023; originally announced July 2023.

Comments: v2. 24 pages. generalized while rule, proved completeness, improved exposition

Can Quantum Computing Improve Uniform Random Sampling of Large Configuration Spaces? (Preprint)

Authors: Joshua Ammermann, Tim Bittner, Domenik Eichhorn, Ina Schaefer, Christoph Seidl

Abstract: A software product line models the variability of highly configurable systems. Complete exploration of all valid configurations (the configuration space) is infeasible as it grows exponentially with the number of features in the worst case. In practice, few representative configurations are sampled instead, which may be used for software testing or hardware verification. Pseudo-randomness of moder… ▽ More A software product line models the variability of highly configurable systems. Complete exploration of all valid configurations (the configuration space) is infeasible as it grows exponentially with the number of features in the worst case. In practice, few representative configurations are sampled instead, which may be used for software testing or hardware verification. Pseudo-randomness of modern computers introduces statistical bias into these samples. Quantum computing enables truly random, uniform configuration sampling based on inherently random quantum physical effects. We propose a method to encode the entire configuration space in a superposition and then measure one random sample. We show the method's uniformity over multiple samples and investigate its scale for different feature models. We discuss the possibilities and limitations of quantum computing for uniform random sampling regarding current and future quantum hardware. △ Less

Submitted 27 July, 2023; originally announced July 2023.

Comments: 8 pages, 5 figures, 2 tables, accepted at Q-SE 2023 (ICSE workshop) and to be published in ICSE-Companion, this is a preprint version before submission

A Query Language for Software Architecture Information (Extended version)

Authors: Joshua Ammermann, Sven Jordan, Lukas Linsbauer, Ina Schaefer

Abstract: Software maintenance is an important part of a software system's life cycle. Maintenance tasks of existing software systems suffer from architecture information that is diverging over time (architectural drift). The Digital Architecture Twin (DArT) can support software maintenance by providing up-to-date architecture information. For this, the DArT gathers such information and co-evolves with a so… ▽ More Software maintenance is an important part of a software system's life cycle. Maintenance tasks of existing software systems suffer from architecture information that is diverging over time (architectural drift). The Digital Architecture Twin (DArT) can support software maintenance by providing up-to-date architecture information. For this, the DArT gathers such information and co-evolves with a software system, enabling continuous reverse engineering. But the crucial link for stakeholders to retrieve this information is missing. To fill this gap, we contribute the Architecture Information Query Language (AIQL), which enables stakeholders to access up-to-date and tailored architecture information. We derived four application scenarios in the context of continuous reverse engineering. We showed that the AIQL provides the required functionality to formulate queries for the application scenarios and that the language scales for use with real-world software systems. In a user study, stakeholders agreed that the language is easy to understand and assessed its value to the specific stakeholder for the application scenarios. △ Less

Submitted 4 July, 2023; v1 submitted 29 June, 2023; originally announced June 2023.

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.

Comments: arXiv admin note: text overlap with arXiv:2204.05644

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 2 (June 7, 2023) lmcs:10384

Model-based Fault Classification for Automotive Software

Authors: Mike Becker, Roland Meyer, Tobias Runge, Ina Schaefer, Sören van der Wall, Sebastian Wolff

Abstract: Intensive testing using model-based approaches is the standard way of demonstrating the correctness of automotive software. Unfortunately, state-of-the-art techniques leave a crucial and labor intensive task to the test engineer: identifying bugs in failing tests. Our contribution is a model-based classification algorithm for failing tests that assists the engineer when identifying bugs. It consis… ▽ More Intensive testing using model-based approaches is the standard way of demonstrating the correctness of automotive software. Unfortunately, state-of-the-art techniques leave a crucial and labor intensive task to the test engineer: identifying bugs in failing tests. Our contribution is a model-based classification algorithm for failing tests that assists the engineer when identifying bugs. It consists of three steps. (i) Fault localization replays the test on the model to identify the moment when the two diverge. (ii) Fault explanation then computes the reason for the divergence. The reason is a subset of actions from the test that is sufficient for divergence. (iii) Fault classification groups together tests that fail for similar reasons. Our approach relies on machinery from formal methods: (i) symbolic execution, (ii) Hoare logic and a new relationship between the intermediary assertions constructed for a test, and (iii) a new relationship among Hoare proofs. A crucial aspect in automotive software is timing requirements, for which we develop appropriate Hoare logic theory. We also briefly report on our prototype implementation for the CAN bus Unified Diagnostic Services in an industrial project. △ Less

Submitted 15 December, 2022; v1 submitted 30 August, 2022; originally announced August 2022.

Information Flow Control-by-Construction for an Object-Oriented Language Using Type Modifiers

Authors: Tobias Runge, Alexander Kittelmann, Marco Servetto, Alex Potanin, Ina Schaefer

Abstract: In security-critical software applications, confidential information must be prevented from leaking to unauthorized sinks. Static analysis techniques are widespread to enforce a secure information flow by checking a program after construction. A drawback of these systems is that incomplete programs during construction cannot be checked properly. The user is not guided to a secure program by most s… ▽ More In security-critical software applications, confidential information must be prevented from leaking to unauthorized sinks. Static analysis techniques are widespread to enforce a secure information flow by checking a program after construction. A drawback of these systems is that incomplete programs during construction cannot be checked properly. The user is not guided to a secure program by most systems. We introduce IFbCOO, an approach that guides users incrementally to a secure implementation by using refinement rules. In each refinement step, confidentiality or integrity (or both) is guaranteed alongside the functional correctness of the program, such that insecure programs are declined by construction. In this work, we formalize IFbCOO and prove soundness of the refinement rules. We implement IFbCOO in the tool CorC and conduct a feasibility study by successfully implementing case studies. △ Less

Submitted 4 August, 2022; originally announced August 2022.

A Specification Logic for Programs in the Probabilistic Guarded Command Language (Extended Version)

Authors: Raúl Pardo, Einar Broch Johnsen, Ina Schaefer, Andrzej Wąsowski

Abstract: The semantics of probabilistic languages has been extensively studied, but specification languages for their properties have received little attention. This paper introduces the probabilistic dynamic logic pDL, a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. The proposed logic pDL can express both first-order state properties and probab… ▽ More The semantics of probabilistic languages has been extensively studied, but specification languages for their properties have received little attention. This paper introduces the probabilistic dynamic logic pDL, a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. The proposed logic pDL can express both first-order state properties and probabilistic reachability properties, addressing both the non-deterministic and probabilistic choice operators of pGCL. In order to precisely explain the meaning of specifications, we formally define the satisfaction relation for pDL. Since pDL embeds pGCL programs in its box-modality operator, pDL satisfiability builds on a formal MDP semantics for pGCL programs. The satisfaction relation is modeled after PCTL, but extended from propositional to first-order setting of dynamic logic, and also embedding program fragments. We study basic properties of pDL, such as weakening and distribution, that can support reasoning systems. Finally, we demonstrate the use of pDL to reason about program behavior. △ Less

Submitted 19 August, 2022; v1 submitted 10 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.

Custom-Tailored Clone Detection for IEC 61131-3 Programming Languages

Authors: Kamil Rosiak, Alexander Schlie, Lukas Linsbauer, Birgit Vogel-Heuser, Ina Schaefer

Abstract: Automated production systems (aPS) are highly customized systems that consist of hardware and software. Such aPS are controlled by a programmable logic controller (PLC), often in accordance with the IEC 61131-3 standard that divides system implementation into so-called program organization units (POUs) as the smallest software unit and is comprised of multiple textual and graphical programming lan… ▽ More Automated production systems (aPS) are highly customized systems that consist of hardware and software. Such aPS are controlled by a programmable logic controller (PLC), often in accordance with the IEC 61131-3 standard that divides system implementation into so-called program organization units (POUs) as the smallest software unit and is comprised of multiple textual and graphical programming languages that can be arbitrarily nested. A common practice during the development of such systems is reusing implementation artifacts by copying, pasting, and then modifying code. This approach is referred to as code cloning. It is used on a fine-granular level where a POU is cloned within a system variant. It is also applied on the coarse-granular system level, where the entire system is cloned and adapted to create a system variant, for example for another customer. This ad hoc practice for the development of variants is commonly referred to as clone-and-own. It allows the fast development of variants to meet varying customer requirements or altered regulatory guidelines. However, clone-and-own is a non-sustainable approach and does not scale with an increasing number of variants. It has a detrimental effect on the overall quality of a software system, such as the propagation of bugs to other variants, which harms maintenance. In order to support the effective development and maintenance of such systems, a detailed code clone analysis is required. On the one hand, an analysis of code clones within a variant (i.e., clone detection in the classical sense) supports experts in refactoring respective code into library components. On the other hand, an analysis of commonalities and differences between cloned variants (i.e., variability analysis) supports the maintenance and further reuse and facilitates the migration of variants into a software product line (SPL). △ Less

Submitted 22 August, 2021; originally announced August 2021.

Comments: JSS: Special Issue on Clone Detection

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.

Comments: In Proceedings F-IDE 2018, arXiv:1811.09014

Journal ref: EPTCS 284, 2018, pp. 53-70

Using Multi-Viewpoint Contracts for Negotiation of Embedded Software Updates

Authors: Sönke Holthusen, Sophie Quinton, Ina Schaefer, Johannes Schlatow, Martin Wegner

Abstract: In this paper we address the issue of change after deployment in safety-critical embedded system applications. Our goal is to substitute lab-based verification with in-field formal analysis to determine whether an update may be safely applied. This is challenging because it requires an automated process able to handle multiple viewpoints such as functional correctness, timing, etc. For this purpos… ▽ More In this paper we address the issue of change after deployment in safety-critical embedded system applications. Our goal is to substitute lab-based verification with in-field formal analysis to determine whether an update may be safely applied. This is challenging because it requires an automated process able to handle multiple viewpoints such as functional correctness, timing, etc. For this purpose, we propose an original methodology for contract-based negotiation of software updates. The use of contracts allows us to cleanly split the verification effort between the lab and the field. In addition, we show how to rely on existing viewpoint-specific methods for update negotiation. We illustrate our approach on a concrete example inspired by the automotive domain. △ Less

Submitted 1 June, 2016; originally announced June 2016.

Comments: In Proceedings PrePost 2016, arXiv:1605.08096

ACM Class: D.2.4

Journal ref: EPTCS 208, 2016, pp. 31-45

Incremental Consistency Checking in Delta-oriented UML-Models for Automation Systems

Authors: Matthias Kowal, Ina Schaefer

Abstract: Automation systems exist in many variants and may evolve over time in order to deal with different environment contexts or to fulfill changing customer requirements. This induces an increased complexity during design-time as well as tedious maintenance efforts. We already proposed a multi-perspective modeling approach to improve the development of such systems. It operates on different levels of a… ▽ More Automation systems exist in many variants and may evolve over time in order to deal with different environment contexts or to fulfill changing customer requirements. This induces an increased complexity during design-time as well as tedious maintenance efforts. We already proposed a multi-perspective modeling approach to improve the development of such systems. It operates on different levels of abstraction by using well-known UML-models with activity, composite structure and state chart models. Each perspective was enriched with delta modeling to manage variability and evolution. As an extension, we now focus on the development of an efficient consistency checking method at several levels to ensure valid variants of the automation system. Consistency checking must be provided for each perspective in isolation, in-between the perspectives as well as after the application of a delta. △ Less

Submitted 1 April, 2016; originally announced April 2016.

Comments: In Proceedings FMSPLE 2016, arXiv:1603.08577

Journal ref: EPTCS 206, 2016, pp. 32-45

Detecting and Explaining Conflicts in Attributed Feature Models

Authors: Uwe Lesta, Ina Schaefer, Tim Winkelmann

Abstract: Product configuration systems are often based on a variability model. The development of a variability model is a time consuming and error-prone process. Considering the ongoing development of products, the variability model has to be adapted frequently. These changes often lead to mistakes, such that some products cannot be derived from the model anymore, that undesired products are derivable or… ▽ More Product configuration systems are often based on a variability model. The development of a variability model is a time consuming and error-prone process. Considering the ongoing development of products, the variability model has to be adapted frequently. These changes often lead to mistakes, such that some products cannot be derived from the model anymore, that undesired products are derivable or that there are contradictions in the variability model. In this paper, we propose an approach to discover and to explain contradictions in attributed feature models efficiently in order to assist the developer with the correction of mistakes. We use extended feature models with attributes and arithmetic constraints, translate them into a constraint satisfaction problem and explore those for contradictions. When a contradiction is found, the constraints are searched for a set of contradicting relations by the QuickXplain algorithm. △ Less

Submitted 14 April, 2015; originally announced April 2015.

Comments: In Proceedings FMSPLE 2015, arXiv:1504.03014

ACM Class: D.2.2; D.2.13

Journal ref: EPTCS 182, 2015, pp. 31-43

Delta Modeling for Software Architectures

Authors: Arne Haber, Holger Rendel, Bernhard Rumpe, Ina Schaefer

Abstract: Architectural modeling is an integral part of modern software development. In particular, diverse systems benefit from precise architectural models since similar components can often be reused between different system variants. However, during all phases of diverse system development, system variability has to be considered and modeled by appropriate means. Delta modeling is a language-independent… ▽ More Architectural modeling is an integral part of modern software development. In particular, diverse systems benefit from precise architectural models since similar components can often be reused between different system variants. However, during all phases of diverse system development, system variability has to be considered and modeled by appropriate means. Delta modeling is a language-independent approach for modeling system variability. A set of diverse systems is represented by a core system and a set of deltas specifying modifications to the core system. In this paper, we give a first sketch of how to apply delta modeling in MontiArc, an existing architecture description language, in order to obtain an integrated modeling language for architectural variability. The developed language, MontiArc, allows the modular modeling of variable software architectures and supports proactive as well as extractive product line development. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 10 pages, 6 figures. > Tagungsband des Dagstuhl-Workshop MBEES: Modellbasierte Entwicklung eingebetteter Systeme VII, fortiss GmbH München, February 2011

Hierarchical Variability Modeling for Software Architectures

Authors: Arne Haber, Holger Renel, Bernhard Rumpe, Ina Schaefer, Frank van der Linden

Abstract: 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 integr… ▽ More 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. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 10 pages, 9 figures. Proceedings of International Software Product Lines Conference (SPLC 2011), IEEE Computer Society, August 2011

Delta-oriented Architectural Variability Using MontiCore

Authors: Arne Haber, Thomas Kutz, Holger Rendel, Bernhard Rumpe, Ina Schaefer

Abstract: Modeling of software architectures is a fundamental part of software development processes. Reuse of software components and early analysis of software topologies allow the reduction of development costs and increases software quality. Integrating variability modeling concepts into architecture description languages (ADLs) is essential for the development of diverse software systems with high dema… ▽ More Modeling of software architectures is a fundamental part of software development processes. Reuse of software components and early analysis of software topologies allow the reduction of development costs and increases software quality. Integrating variability modeling concepts into architecture description languages (ADLs) is essential for the development of diverse software systems with high demands on software quality. In this paper, we present the integration of delta modeling into the existing ADL MontiArc. Delta modeling is a language-independent variability modeling approach supporting proactive, reactive and extractive product line development. We show how ?-MontiArc, a language for explicit modeling of architectural variability based on delta modeling, is implemented as domain-specific language (DSL) using the DSL development framework MontiCore. We also demonstrate how MontiCore's language reuse mechanisms provide efficient means to derive an implementation of ?-MontiArc tool implementation. We evaluate ?-Monti-Arc by comparing it with annotative variability modeling. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 10 pages, 9 figures. ECSA '11 5th European Conference on Software Architecture: Companion Volume, ACM New York, NY, USA, Article No. 6, September 2011

Towards a Family-based Analysis of Applicability Conditions in Architectural Delta Models

Authors: Arne Haber, Thomas Kutz, Holger Rendel, Bernhard Rumpe, Ina Schaefer

Abstract: Modeling variability in software architectures is a fundamental part of software product line development. ?-MontiArc allows describing architectural variability in a modular way by a designated core architecture and a set of architectural delta models modifying the core architecture to realize other architecture variants. Delta models have to satisfy a set of applicability conditions for the defi… ▽ More Modeling variability in software architectures is a fundamental part of software product line development. ?-MontiArc allows describing architectural variability in a modular way by a designated core architecture and a set of architectural delta models modifying the core architecture to realize other architecture variants. Delta models have to satisfy a set of applicability conditions for the definedness of the architectural variants. The applicability conditions can in principle be checked by generating all possible architecture variants, which requires considering the same intermediate architectures repeatedly. In order to reuse previously computed architecture variants, we propose a family-based analysis of the applicability conditions using the concept of inverse deltas. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 10 pages, 7 figures. Variability for You Proceedings of VARY InternationalWorkshop affiliated with ACM/IEEE 14th International Conference on Model Driven Engineering Languages and Systems (MODELS'11), IT University Technical Report Series TR-2011-144

Report number: TR-2011-144

Evolving Delta-oriented Software Product Line Architectures

Authors: Arne Haber, Holger Renel, Bernhard Rumpe, Ina Schaefer

Abstract: Diversity is prevalent in modern software systems. Several system variants exist at the same time in order to adapt to changing user requirements. Additionally, software systems evolve over time in order to adjust to unanticipated changes in their application environment. In modern software development, software architecture modeling is an important means to deal with system complexity by architec… ▽ More Diversity is prevalent in modern software systems. Several system variants exist at the same time in order to adapt to changing user requirements. Additionally, software systems evolve over time in order to adjust to unanticipated changes in their application environment. In modern software development, software architecture modeling is an important means to deal with system complexity by architectural decomposition. This leads to the need of architectural description languages that can represent spatial and temporal variability. In this paper, we present delta modeling of software architectures as a uniform modeling formalism for architectural variability in space and in time. In order to avoid degeneration of the product line model under system evolution, we present refactoring techniques to maintain and improve the quality of the variability model. Using a running example from the automotive domain, we evaluate our approach by carrying out a case study that compares delta modeling with annotative variability modeling. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 26 pages, 6 figures

Journal ref: Large-Scale Complex IT Systems. Development, Operation and Management, 17th Monterey Workshop 2012, Oxford, UK, March 19-21, 2012. LNCS Vol. 7539, pp. 183-208

Engineering Delta Modeling Languages

Authors: Arne Haber, Katrin Hölldobler, Carsten Kolassa, Markus Look, Klaus Müller, Bernhard Rumpe, Ina Schaefer

Abstract: 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 larg… ▽ More 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. △ Less

Submitted 25 August, 2014; originally announced August 2014.

Comments: 10 pages, 8 figures. Proceedings of the 17th International Software Product Line Conference, Tokyo, September 2013, pp.22-31, ACM, 2013

ACM Class: D.2; D.2.2; D.2.3

Journal ref: Proceedings of the 17th International Software Product Line Conference, Tokyo, September 2013, pp.22-31, ACM, 2013

First-Class Variability Modeling in Matlab/Simulink

Authors: Arne Haber, Carsten Kolassa, Peter Manhart, Pedram Mir Seyed Nazari, Bernhard Rumpe, Ina Schaefer

Abstract: Modern cars exist in an vast number of variants. Thus, variability has to be dealt with in all phases of the development process, in particular during model-based development of software-intensive functionality using Matlab/Simulink. Currently, variability is often encoded within a functional model leading to so called 150%-models which easily become very complex and do not scale for larger produc… ▽ More Modern cars exist in an vast number of variants. Thus, variability has to be dealt with in all phases of the development process, in particular during model-based development of software-intensive functionality using Matlab/Simulink. Currently, variability is often encoded within a functional model leading to so called 150%-models which easily become very complex and do not scale for larger product lines. To counter these problems, we propose a modular variability modeling approach for Matlab/Simulink based on the concept of delta modeling [8, 9, 24]. A functional variant is described by a delta encapsulating a set of modifications. A sequence of deltas can be applied to a core product to derive the desired variant. We present a prototypical implementation, which is integrated into Matlab/Simulink and offers graphical editing of delta models. △ Less

Submitted 25 August, 2014; originally announced August 2014.

Comments: 8 pages, 8 figures. Workshop on Variability Modelling of Software-intensive Systems. VaMoS 2013 in Pisa, Italy

ACM Class: D.2.6; D.2.2

Journal ref: Proceedings of the Seventh International Workshop on Variability Modelling of Software-intensive Systems, 23.-25.1.2013, pp. 11-18, ACM, New York, NY, USA. 2013