-
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.
-
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.
-
Coherent manipulation of nuclear spins in the strong driving regime
Authors:
Dan Yudilevich,
Alon Salhov,
Ido Schaefer,
Konstantin Herb,
Alex Retzker,
Amit Finkler
Abstract:
Spin-based quantum information processing makes extensive use of spin-state manipulation. This ranges from dynamical decoupling of nuclear spins in quantum sensing experiments to applying logical gates on qubits in a quantum processor. Here we present an antenna for strong driving in quantum sensing experiments and theoretically address challenges of the strong driving regime. First, we designed a…
▽ More
Spin-based quantum information processing makes extensive use of spin-state manipulation. This ranges from dynamical decoupling of nuclear spins in quantum sensing experiments to applying logical gates on qubits in a quantum processor. Here we present an antenna for strong driving in quantum sensing experiments and theoretically address challenges of the strong driving regime. First, we designed and implemented a micron-scale planar spiral RF antenna capable of delivering intense fields to a sample. The planar antenna is tailored for quantum sensing experiments using the diamond's nitrogen-vacancy (NV) center and should be applicable to other solid-state defects. The antenna has a broad bandwidth of 22 MHz, is compatible with scanning probes, and is suitable for cryogenic and ultrahigh vacuum conditions. We measure the magnetic field induced by the antenna and estimate a field-to-current ratio of $113\pm 16$ G/A, representing a x6 increase in efficiency compared to the state-of-the-art. We demonstrate the antenna by driving Rabi oscillations in $^1$H spins of an organic sample on the diamond surface and measure $^1$H Rabi frequencies of over 500 kHz, i.e., $\mathrmπ$-pulses shorter than 1 $μs$ - faster than previously reported in NV-based nuclear magnetic resonance (NMR). Finally, we discuss the implications of driving spins with a field tilted from the transverse plane in a regime where the driving amplitude is comparable to the spin-state splitting, such that the rotating wave approximation does not describe the dynamics well. We present a recipe to optimize pulse fidelity in this regime based on a phase and offset-shifted sine drive, that may be optimized without numerical optimization procedures or precise modeling of the experiment. We consider this approach in a range of driving amplitudes and show that it is particularly efficient in the case of a tilted driving field.
△ Less
Submitted 31 October, 2023;
originally announced October 2023.
-
PARMESAN: Meteorological Timeseries and Turbulence Analysis Backed by Symbolic Mathematics
Authors:
Yann Georg Büchau,
Hasan Mashni,
Matteo Bramati,
Vasileios Savvakis,
Ines Schäfer,
Saskia Jung,
Gabriela Miranda-Garcia,
Daniel Hardt,
Jens Bange
Abstract:
PARMESAN (the Python Atmospheric Research Package for MEteorological TimeSeries and Turbulence ANalysis) is a Python package providing common functionality for atmospheric scientists doing time series or turbulence analysis. Several meteorological quantities such as potential temperature, various humidity measures, gas concentrations, wind speed and direction, turbulence and stability parameters c…
▽ More
PARMESAN (the Python Atmospheric Research Package for MEteorological TimeSeries and Turbulence ANalysis) is a Python package providing common functionality for atmospheric scientists doing time series or turbulence analysis. Several meteorological quantities such as potential temperature, various humidity measures, gas concentrations, wind speed and direction, turbulence and stability parameters can be calculated. Furthermore, signal processing functionality such as properly normed variance spectra for frequency analysis is available. In contrast to existing packages with similar goals, its routines for physical quantities are derived from symbolic mathematical expressions, enabling inspection, automatic rearrangement, reuse and recombination of the underlying equations. Building on this, PARMESAN's functions as well as their comprehensive parameter documentation are mostly auto-generated, minimizing human error and effort. In addition, sensitivity/error propagation analysis is possible as mathematical operations like derivations can be applied to the underlying equations. Physical consistency in terms of units and value domains are transparently ensured for PARMESAN functions. PARMESAN's approach can be reused to simplify implementation of robust routines in other fields of physics.
△ Less
Submitted 26 September, 2023;
originally announced September 2023.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
Optimization of high-order harmonic generation by optimal control theory: Ascending a functional landscape in extreme conditions
Authors:
Ido Schaefer,
Ronnie Kosloff
Abstract:
A theoretical optimization method of high-harmonic-generation (HHG) is developed in the framework of optimal-control-theory (OCT). The target of optimization is the emission radiation of a particular frequency. The OCT formulation includes restrictions on the frequency band of the driving pulse, the permanent ionization probability and the total energy of the driving pulse. The optimization task r…
▽ More
A theoretical optimization method of high-harmonic-generation (HHG) is developed in the framework of optimal-control-theory (OCT). The target of optimization is the emission radiation of a particular frequency. The OCT formulation includes restrictions on the frequency band of the driving pulse, the permanent ionization probability and the total energy of the driving pulse. The optimization task requires a highly accurate simulation of the dynamics. Absorbing boundary conditions are employed, where a complex-absorbing-potential is constructed by an optimization scheme for maximization of the absorption. A new highly accurate propagation scheme is employed, which can address explicit time dependence of the driving as well as a non-Hermitian Hamiltonian. The optimization process is performed by a second-order gradient scheme. The method is applied to a simple one-dimensional model system. The results demonstrate a significant enhancement of selected harmonics, with minimized total energy of the driving pulse and controlled permanent ionization probability. A successful enhancement of an even harmonic emission is also demonstrated.
△ Less
Submitted 13 February, 2020; v1 submitted 19 June, 2019;
originally announced June 2019.
-
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.
-
Semi-global approach for propagation of the time-dependent Schrödinger equation for time-dependent and nonlinear problems
Authors:
Ido Schaefer,
Hillel Tal-Ezer,
Ronnie Kosloff
Abstract:
A detailed exposition of highly efficient and accurate method for the propagation of the time-dependent Schrödinger equation is presented. The method is readily generalized to solve an arbitrary set of ODE's. The propagation is based on a global approach, in which large time-intervals are treated as a whole, replacing the local considerations of the common propagators. The new method is suitable f…
▽ More
A detailed exposition of highly efficient and accurate method for the propagation of the time-dependent Schrödinger equation is presented. The method is readily generalized to solve an arbitrary set of ODE's. The propagation is based on a global approach, in which large time-intervals are treated as a whole, replacing the local considerations of the common propagators. The new method is suitable for various classes of problems, including problems with a time-dependent Hamiltonian, nonlinear problems, non-Hermitian problems and problems with an inhomogeneous source term. In this paper, a thorough presentation of the basic principles of the propagator is given. We give also a special emphasis on the details of the numerical implementation of the method. For the first time, we present the application for a non-Hermitian problem by a numerical example of a one-dimensional atom under the influence of an intense laser field. The efficiency of the method is demonstrated by a comparison with the common Runge-Kutta approach.
△ Less
Submitted 1 May, 2017; v1 submitted 21 November, 2016;
originally announced November 2016.
-
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.
-
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.
-
Three approaches for representing Lindblad dynamics by a matrix-vector notation
Authors:
Morag Am-Shallem,
Amikam Levy,
Ido Schaefer,
Ronnie Kosloff
Abstract:
Markovian dynamics of open quantum systems are described by the L-GKS equation, known also as the Lindblad equation. The equation is expressed by means of left and right matrix multiplications. This formulation hampers numerical implementations. Representing the dynamics by a matrix-vector notation overcomes this problem. We review three approaches to obtain such a representation. The methods are…
▽ More
Markovian dynamics of open quantum systems are described by the L-GKS equation, known also as the Lindblad equation. The equation is expressed by means of left and right matrix multiplications. This formulation hampers numerical implementations. Representing the dynamics by a matrix-vector notation overcomes this problem. We review three approaches to obtain such a representation. The methods are demonstrated for a driven two-level system subject to spontaneous emission.
△ Less
Submitted 10 December, 2015; v1 submitted 29 October, 2015;
originally announced October 2015.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
Optimal control theory of harmonic generation
Authors:
Ido Schaefer,
Ronnie Kosloff
Abstract:
Coherent control of harmonic generation was studied theoretically. A specific harmonic order was targeted. An optimal control theory was employed to find the driving field where restrictions were imposed on the frequency band. Additional restrictions were added to suppress undesired outcomes such as ionization and dissociation. The method was formulated in the frequency domain. An update procedure…
▽ More
Coherent control of harmonic generation was studied theoretically. A specific harmonic order was targeted. An optimal control theory was employed to find the driving field where restrictions were imposed on the frequency band. Additional restrictions were added to suppress undesired outcomes such as ionization and dissociation. The method was formulated in the frequency domain. An update procedure for the field based on relaxation was employed. The method was tested on several examples demonstrating generation of high frequencies from a driving field with a restricted frequency band.
△ Less
Submitted 3 January, 2013; v1 submitted 28 August, 2012;
originally announced August 2012.
-
New, Highly Accurate Propagator for the Linear and Nonlinear Schrödinger Equation
Authors:
Hillel Tal-Ezer,
Ronnie Kosloff,
Ido Schaefer
Abstract:
A propagation method for the time dependent Schrödinger equation was studied leading to a general scheme of solving ode type equations. Standard space discretization of time-dependent pde's usually results in system of ode's of the form u_t -Gu = s where G is a operator (matrix) and u is a time-dependent solution vector. Highly accurate methods, based on polynomial approximation of a modified expo…
▽ More
A propagation method for the time dependent Schrödinger equation was studied leading to a general scheme of solving ode type equations. Standard space discretization of time-dependent pde's usually results in system of ode's of the form u_t -Gu = s where G is a operator (matrix) and u is a time-dependent solution vector. Highly accurate methods, based on polynomial approximation of a modified exponential evolution operator, had been developed already for this type of problems where G is a linear, time independent matrix and s is a constant vector. In this paper we will describe a new algorithm for the more general case where s is a time-dependent r.h.s vector. An iterative version of the new algorithm can be applied to the general case where G depends on t or u. Numerical results for Schrödinger equation with time-dependent potential and to non-linear Schrödinger equation will be presented.
△ Less
Submitted 17 April, 2012;
originally announced April 2012.
-
Quantum Optimal Control Theory of Harmonic Generation
Authors:
Ido Schaefer
Abstract:
A new method for controlling harmonic generation, in the framework of quantum optimal control theory (QOCT), is developed. The problem is formulated in the frequency domain using a new maximization functional. The relaxation method is used as the optimization procedure. The new formulation is generalized to other control problems with requirements in the frequency domain. The method is applied to…
▽ More
A new method for controlling harmonic generation, in the framework of quantum optimal control theory (QOCT), is developed. The problem is formulated in the frequency domain using a new maximization functional. The relaxation method is used as the optimization procedure. The new formulation is generalized to other control problems with requirements in the frequency domain. The method is applied to several simple problems. The results are analysed and discussed. General conclusions on harmonic generation mechanisms are obtained.
△ Less
Submitted 27 August, 2012; v1 submitted 29 February, 2012;
originally announced February 2012.
-
Representation Theoretical Construction of the Classical Limit and Spectral Statistics of Generic Hamiltonian Operators
Authors:
Ingolf Schäfer
Abstract:
Starting with an operator in the universal envelo** algebra of a semi-simple, complex Lie group the nearest neighbor statistics of the spectra of this operator along a sequence of representations are discussed.
After a short introduction in chapter 1 this problem is motivated by a general construction of the classical limit for quantum mechanical systems, which is adopted to this setting, in…
▽ More
Starting with an operator in the universal envelo** algebra of a semi-simple, complex Lie group the nearest neighbor statistics of the spectra of this operator along a sequence of representations are discussed.
After a short introduction in chapter 1 this problem is motivated by a general construction of the classical limit for quantum mechanical systems, which is adopted to this setting, in chapter 2. In chapter 3 it is shown that for simple operators, i.e., operators of the Lie algebra the nearest neighbor statistics along a sequence of irreducible representations converge to the Dirac measure. After a suitable completion of the universal envelo** algebra the convergence to Poisson statistics is proved in chapter 4 for the exponentials of generic operators. The proof makes use of a combinatorial inequality of the Katz-Sarnak type for tori, which is proved in chapter 5. In the appendix the necessary facts from group theory and the theory of nearest neighbor distributions are gathered.
△ Less
Submitted 27 December, 2006;
originally announced December 2006.
-
Constructing the classical limit for quantum systems on compact semisimple Lie algebras
Authors:
I. Schafer,
M. Kus
Abstract:
We give a general construction for the classical limit of a quantum system defined in terms of generators of an arbitrary compact semisimple Lie algebra, generalizing known results for the $\mathfrak{su}_2$ and $\mathfrak{su}_3$ cases. The classical limit depends on the physical problem in question and is determined by the sequence of representations by which it is reached. Only in the simplest…
▽ More
We give a general construction for the classical limit of a quantum system defined in terms of generators of an arbitrary compact semisimple Lie algebra, generalizing known results for the $\mathfrak{su}_2$ and $\mathfrak{su}_3$ cases. The classical limit depends on the physical problem in question and is determined by the sequence of representations by which it is reached. Only in the simplest cases it is unique. We present explicit formulae useful in determining the classical limit in all important cases.
△ Less
Submitted 5 April, 2006;
originally announced April 2006.