In its quest for approaches to taming uncertainty in self-adaptive systems (SAS), the research community has largely focused on solutions that adapt the SAS architecture or behaviour in response to uncertainty. By comparison, solutions that reduce the uncertainty affecting SAS (other than through the blanket monitoring of their components and environment) remain underexplored. Our previous work proposed Parley , a more nuanced, adaptive approach to SAS uncertainty reduction. To that end, we introduced an SAS architecture comprising an uncertainty reduction controller that drives the adaptive acquisition of new information within the SAS adaptation loop and a tool-supported method that uses probabilistic model checking to synthesise such controllers. The controllers generated by our method deliver optimal tradeoffs between SAS uncertainty reduction benefits and new information acquisition costs with guarantees for the satisfaction of requirements. In this article, we extend Parley to Parley+ by improving the synthesis of these controllers and by expanding the formalisation of Parley+ to prove the validity of the synthesis. We illustrate the use and extend the evaluation of the effectiveness of our approach for mobile robot navigation and service-based system SAS. The evaluation results show that Parley+ can synthesise controllers that help achieve the system’s objectives significantly better than Parley in 88.1% of the cases.

Mispredictions by machine learning components can have severe consequences, especially in safety-critical and mission-critical software systems. Therefore, understanding and debugging these mispredictions is a crucial part of the development process for systems that use machine learning components. Previous research has successfully applied methods that identify when a model’s predictions may be unreliable by generating a rule set that links feature values to prediction errors. However, current state-of-the-art rule set approaches require significant computational resources, particularly for large data setsTo address these high computational demands, we propose a strategy to identify and focus only on the most influential features that lead to mispredictions. Additionally, to improve the accuracy of mispredictions diagnosis, we replace traditional rule-based approaches with decision tree learning. We evaluate our tool MMDFAST across 11 diverse real-world data sets. The results show that focusing on influential features with decision trees improves the accuracy of misprediction explanations, while significantly reducing computational demands in all scenarios. Thus, MMDFAST produces better results much faster, making it more efficient and effective for generating misprediction explanations.

Program fixes must preserve passing tests while fixing failing ones. Validating these properties requires test oracles that distinguish passing from failing runs.We introduce BASHIRI, a tool that learns failure oracles from test suites with labeled outcomes using execution features. BASHIRI leverages execution-feature-driven debugging to collect program execution features and trains interpretable models as testing oracles. Our evaluation shows that BASHIRI predicts test outcomes with 95% accuracy, effectively identifying failing runs. BASHIRI is available as an open-source tool at https://github.com/smythi93/bashiriA demonstration video is available at https://youtu.be/D2mJkCtSXtM

Personas offer an empathetic approach to capturing user requirements, translating user needs into relatable narratives. However, creating personas manually is time-consuming. Large Language Models (LLMs) can generate personas with convincing natural language, challenging traditional methods. Yet, LLM-generated personas may reflect biases from their training data, potentially compromising diversity. Our study explores how diversity is considered in LLM-generated personas through a qualitative user study with 22 participants. Participants generated personas without specific diversity prompts in the first task, revealing how users naturally interact with LLMs. In the second task, participants were explicitly asked to consider diversity aspects when prompting for personas. Analyzing the prompts and outputs showed that users tend to request less diversity unless explicitly instructed. Meanwhile, LLMs can introduce diversity even when not prompted, potentially broadening representation. However, we also found a critical pitfall: LLM-generated personas may appear diverse due to mentioning various aspects, but fail to translate them into meaningful implications for requirements engineering. This shows the need for a more deliberate approach when using LLMs for persona creation to ensure diversity is not just performative but genuinely informative for design and development.

Deep learning (DL) components have been broadly applied in diverse applications. Similar to traditional software engineering, effective test case generation methods are needed by industry to enhance the quality and robustness of these deep learning components. To this end, we propose a novel automatic software testing technique, TAEFuzz (Automatic Fuzz -Testing via T ransferable A dversarial E xamples), which aims to automatically assess and enhance the robustness of image-based deep learning (DL) systems based on test cases generated by transferable adversarial examples. TAEFuzz alleviates the over-fitting problem during optimized test case generation and prevents test cases from prematurely falling into local optima. In addition, TAEFuzz enhances the visual quality of test cases through constraining perturbations inserted into sensitive areas of the images. For a system with low robustness, TAEFuzz trains a low-cost denoising module to reduce the impact of perturbations in transferable adversarial examples on the system. Experimental results demonstrate that the test cases generated by TAEFuzz can discover up to 46.1% more errors in the targeted systems, and ensure the visual quality of test cases. Compared to existing techniques, TAEFuzz also enhances the robustness of the target systems against transferable adversarial examples with the perturbation denoising module.

We consider the use of concept bottleneck models (CBMs) to enhance safety argumentation for classification tasks in safety-critical systems. When constructing a safety argumentation for Machine Learning (ML) models, there exists a semantic gap between the specified behaviour, given through class labels at training time, and the learnt behaviour, measured through performance metrics. We address this gap by using CBMs, a class of interpretable ML models in which the predictions rely on a set of human-defined concepts. A Goal Structuring Notation (GSN)-based safety assurance case is constructed including such concepts, allowing traceability between the system specification and the behaviour of the model. As a result, a line of safety argumentation is provided that relies on the interpretable model trained to satisfy the specified safety requirements.

In recent years, automatic program repair has gained much attention in the research community. Generally, program repair approaches consider a faulty program and a test suite that captures the program's intended behavior. The goal is automatically generating a patch that corrects the fault by identifying the faulty code locations, suggesting a candidate fix, and validating it against the provided tests. However, most existing program repair tools focus on Java or C programs, while Python, one of the most popular programming languages, lacks approaches that work on it.

Identifying and fixing bugs in programs remains a challenge and is one of the most time-consuming tasks in software development. But even after a bug is identified, and a fix has been proposed by a developer or tool, it is not uncommon that the fix is incomplete and does not cover all possible inputs that trigger the bug. This can happen quite often and leads to re-opened issues and inefficiencies. In this paper, we introduce P3, a curated dataset composed of incomplete fixes. Each entry in the set contains a series of commits fixing the same underlying issue, where multiple of the intermediate commits are incomplete fixes. These are sourced from real-world open-source C projects. The selection process involves both automated and manual stages. Initially, we employ heuristics to identify potential partial fixes from repositories, subsequently we validate them through meticulous manual inspection. This process ensures the accuracy and reliability of our curated dataset. We envision that the dataset will support researchers while investigating partial fixes in more detail, allowing them to develop new techniques to detect and fix them. We make our dataset publicly available at https://gitlab.com/sosy-lab/research/data/partial-fix-dataset.

Abstract Context Computational materials science (CMS) focuses on in silico experiments to compute the properties of known and novel materials, where many software packages are used in the community. The NOMAD Laboratory (Draxl C, Scheffler) offers to store the input and output files in its FAIR data repository. Since the file formats of these software packages are non‐standardized, parsers are used to provide the results in a normalized format. Objective The main goal of this article is to report experience and findings of using grammar‐based fuzzing on these parsers. Method We have constructed an input grammar for four common software packages in the CMS domain and performed an experimental evaluation on the capabilities of grammar‐based fuzzing to detect failures in the Novel Materials Discovery (NOMAD) parsers. Results With our approach, we were able to identify three unique critical bugs concerning service availability, as well as several additional syntactic, semantic, logical, and downstream bugs in the investigated NOMAD parsers. We reported all issues to the developer team prior to publication. Conclusion Based on the experience gained, we can recommend grammar‐based fuzzing also for other research software packages to improve the trust level in the correctness of the produced results.

Software systems enabling large-scale data analysis workflows (DAWs) are a key technology for modern science as they allow extracting new insights from experimental results. DAWs are pipelines composed of interdependent tasks that are executed in a distributed fashion on large compute clusters. Typically, the individual task implementations are developed by research groups all over the world and usually not tested outside a narrow scope of possible inputs, parameters, and infrastructures. As a result, the operations' correctness depends on many implicit assumptions, such as the completeness and suitability of input data, infrastructure properties such as available cores, etc. This makes quality assurance of DAWs a critical issue. We propose to address this problem by introducing a contract-driven approach to DAW design and implementation. Following the well-known principle of Design by Contract, DAW developers specify contracts in the form of requirements and promises for each task of a DAW. These contracts serve as guards to ensure that tasks run in a proper environment and produce correct results. The detection of contract violations allows to halt the execution of a DAW and to identify the culprit that caused the violation. Thus, the integration of contracts into DAW design provides opportunities for efficiency improvements by reducing computation and debugging time in case of errors.

Software systems enabling large-scale data analysis workflows (DAWs) are a key technology for many scientific disciplines, as they allow extracting new insights from experimental results. DAWs are (non-)linear pipelines composed of multiple interdependent tasks that are executed in a distributed fashion on large compute clusters. In science, the individual task implementations are developed by research groups all over the world and usually not tested outside a narrow scope of possible inputs, parameters, and infrastructures. As a result, the operations' correctness depends on many implicit assumptions. Among others this includes the completeness and suitability of input data, infrastructure properties such as available cores or main memory, etc. This combination of complexity, distribution and untested components makes quality assurance of DAWs a critical issue. In this paper, we propose to address this problem by introducing a contract-driven approach to DAW design and implementation. Following this method, DAW developers specify contracts in the form of requirements and promises for each task of a DAW. These contracts serve as guards to ensure that tasks run in a proper environment and produce correct results. We provide the first formal definition of contracts for DAWs and show how they are connected to DAW scheduling and execution. As a proof of concept, we extended Nextflow, a popular scientific workflow system, with contracts and defined a light-weight DSL for their specification. We exemplify the power of a contract-driven approach to DAW development by enhancing several real-world DAWs from Bioinformatics to capture typical problems during their execution and show how the specific notifications issued by broken contracts help debugging the DAWs.

To accurately make adaptation decisions, a self-adaptive system needs precise means to analyze itself at runtime. To this end, runtime verification can be used in the feedback loop to check that the managed system satisfies its requirements formalized as temporal-logic properties. These requirements, however, may change due to system evolution or uncertainty in the environment, managed system, and requirements themselves. Thus, the properties under investigation by the runtime verification have to be dynamically adapted to represent the changing requirements while preserving the knowledge about requirements satisfaction gathered thus far, all with minimal latency. To address this need, we present a runtime verification approach for self-adaptive systems with changing requirements. Our approach uses property specification patterns to automatically obtain automata with precise semantics that are the basis for runtime verification. The automata can be safely adapted during runtime verification while preserving intermediate verification results to seamlessly reflect requirement changes and enable continuous verification. We evaluate our approach on an Arduino prototype of the Body Sensor Network and the Timescales benchmark. Results show that our approach is over five times faster than the typical approach of redeploying and restarting runtime monitors to reflect requirements changes, while improving the system’s trustworthiness by avoiding interruptions of verification.

Why does my program fail? We present a novel and general technique to automatically determine failure causes and conditions, using logical properties over input elements: “The program fails if and only if int( ) > len( ) holds—that is, the given is larger than the length.” Our AVICENNA prototype uses modern techniques for inferring properties of passing and failing inputs and validating and refining hypotheses by having a constraint solver generate supporting test cases to obtain such diagnoses. As a result, AVICENNA produces crisp and expressive diagnoses even for complex failure conditions, considerably improving over the state of the art with diagnoses close to those of human experts.

Abstract Context Ensuring safety for any sophisticated system is getting more complex due to the rising number of features and functionalities. This calls for formal methods to entrust confidence in such systems. Nevertheless, using formal methods in industry is demanding because of their lack of usability and the difficulty of understanding verification results. Objective We evaluate the acceptance of formal methods by Bosch automotive engineers, particularly whether the difficulty of understanding verification results can be reduced. Method We perform two different exploratory studies. First, we conduct a user survey to explore challenges in identifying inconsistent specifications and using formal methods by Bosch automotive engineers. Second, we perform a one-group pretest-posttest experiment to collect impressions from Bosch engineers familiar with formal methods to evaluate whether understanding verification results is simplified by our counterexample explanation approach. Results The results from the user survey indicate that identifying refinement inconsistencies, understanding formal notations, and interpreting verification results are challenging. Nevertheless, engineers are still interested in using formal methods in real-world development processes because it could reduce the manual effort for verification. Additionally, they also believe formal methods could make the system safer. Furthermore, the one-group pretest-posttest experiment results indicate that engineers are more comfortable understanding the counterexample explanation than the raw model checker output. Limitations The main limitation of this study is the generalizability beyond the target group of Bosch automotive engineers.

Abstract Model matching algorithms are used to identify common elements in input models, which is a fundamental precondition for many software engineering tasks, such as merging software variants or views. If there are multiple input models, an n-way matching algorithm that simultaneously processes all models typically produces better results than the sequential application of two-way matching algorithms. However, existing algorithms for n-way matching do not scale well, as the computational effort grows fast in the number of models and their size. We propose a scalable n-way model matching algorithm, which uses multi-dimensional search trees for efficiently finding suitable match candidates through range queries. We implemented our generic algorithm named RaQuN (Range Queries on $$\text {N}$$ N input models) in Java and empirically evaluate the matching quality and runtime performance on several datasets of different origins and model types. Compared to the state of the art, our experimental results show a performance improvement by an order of magnitude, while delivering matching results of better quality.

Abstract Test case generation techniques based on adversarial examples are commonly used to enhance the reliability and robustness of image‐based and text‐based machine learning applications. However, efficient techniques for speech recognition systems are still absent. This paper proposes a family of methods that generate targeted adversarial examples for speech recognition systems. All are based on thefirefly algorithm (F), and are enhanced withgaussmutations and / orgradientestimation (F‐GM, F‐GE, F‐GMGE) to fit the specific problem of targeted adversarial test case generation. We conduct an experimental evaluation on three different types of speech datasets, includingGoogle Command,Common VoiceandLibriSpeech. In addition, we recruit volunteers to evaluate the performance of the adversarial examples. The experimental results show that, compared with existing approaches, these approaches can effectively improve the success rate of the targeted adversarial example generation. The code is publicly available at https://github.com/HanboCai/FGMGE .

Software testing is an important part of the software life-cycle. Unfortunately, some software systems have the inherent problem, that it is not clear a priori what the expected outcome is. This is known in the literature as the Oracle Problem. Scientific software suffers from this problem in particular. Metamorphic Testing is a testing approach that mitigates the Oracle Problem, as it is based on identified relations between a program's in- and output pairs. In this study, we investigate the feasibility of automatically finding such metamorphic relations on a software package known as the exciting-NOMAD parser which is widely used in computational material science. We are able to show that it is indeed possible to automatically find metamorphic relations within the NOMAD parser for the density functional theory code exciting. We analyse the metamorphic relations found through our tool in terms of both quantity and relation quality. Furthermore, we also publish our developed tool, as well as used data alongside this study through our replication package.

A popular metric to evaluate the performance of fuzzers is branch coverage. However, we argue that focusing solely on covering many different branches (i.e., the richness) is not sufficient since the majority of the covered branches may have been exercised only once, which does not inspire a high confidence in the reliability of the covered code. Instead, the distribution of the executed branches (i.e., the evenness) should also be considered. That is, behavioral diversity is only given if the generated inputs not only trigger many different branches, but also trigger them evenly often with diverse inputs. We introduce BeDivFuzz, a feedback-driven fuzzing technique for generator-based fuzzers. BeDivFuzz distinguishes between structure-preserving and structure-changing mutations in the space of syntactically valid inputs, and biases its mutation strategy towards validity and behavioral diversity based on the received program feedback. We have evaluated BeDivFuzz on Ant, Maven, Rhino, Closure, Nashorn, and Tomcat. The results show that BeDivFuzz achieves better behavioral diversity than the state of the art, measured by established biodiversity metrics, namely the Hill numbers, from the field of ecology.

Grammarscan serve asproducersfor structured test inputs that are syntactically correct by construction. A probabilistic grammar assigns probabilities to individual productions, thus controlling the distribution of input elements. Using the grammars as input parsers, we show how tolearn input distributions from input samples,allowing to create inputs that aresimilarto the sample; byinvertingthe probabilities, we can create inputs that aredissimilarto the sample. This allows for threetest generation strategies: 1) “Common inputs”–by learning from common inputs, we can create inputs that aresimilarto the sample; this is useful for regression testing. 2) “Uncommon inputs”–learning from common inputs and inverting probabilities yields inputs that arestrongly dissimilarto the sample; this is useful for completing a test suite with “inputs from hell” that test uncommon features, yet are syntactically valid. 3) “Failure-inducing inputs”–learning from inputs that caused failures in the past gives us inputs that share similar features and thus also have ahigh chance of triggering bugs; this is useful for testing the completeness of fixes. Our evaluation on three common input formats (JSON, JavaScript, CSS) shows the effectiveness of these approaches. Results show that “common inputs” reproduced 96 percent of the methods induced by the samples. In contrast, for almost all subjects (95 percent), the “uncommon inputs” covered significantly different methods from the samples. Learning from failure-inducing samples reproduced all exceptions (100 percent) triggered by the failure-inducing samples and discovered new exceptions not found in any of the samples learned from.

The comparison of a model of a process against event data recorded during its execution, known as conformance checking, is an important means in process analysis. Yet, common conformance checking techniques are computationally expensive, which makes a complete analysis infeasible for large logs. To mitigate this problem, existing techniques leverage data samples. Then, the result quality depends on the relevance of the sample for a specific analysis task. Existing sampling strategies therefore rely on a static assumption on what constitutes relevant event data, which is generally unknown a priori.In this paper, we present relevance-guided sampling of event logs. Instead of employing a fixed relevance hypothesis, our approach learns the characteristics of event data that determine its relevance for conformance checking. To this end, we first explore the correlations between characteristics of the event data and the goal of a conformance checking task, before exploiting these correlations to guide the selection of a data sample. We present different instantiations of this approach and demonstrate that they significantly improve the quality of samples, and hence of conformance checking results, compared to baseline strategies.

Model matching algorithms are used to identify common elements in input models, which is a fundamental precondition for many software engineering tasks, such as merging software variants or views. If there are multiple input models, an n-way matching algorithm that simultaneously processes all models typically produces better results than the sequential application of two-way matching algorithms. However, existing algorithms for n-way matching do not scale well, as the computational effort grows fast in the number of models and their size. We propose a scalable n-way model matching algorithm, which uses multi-dimensional search trees for efficiently finding suitable match candidates through range queries. We implemented our generic algorithm named RaQuN (Range Queries on N input models) in Java, and empirically evaluate the matching quality and runtime performance on several datasets of different origin and model type. Compared to the state-of-the-art, our experimental results show a performance improvement by an order of magnitude, while delivering matching results of better quality.

Automated program repair reduces the manual effort in fixing program errors. However, existing repair techniques modify a buggy program such that it passes given tests. Such repair techniques do not discriminate between correct patches and patches that overfit the available tests (breaking untested but desired functionality). We propose an integrated approach for detecting and discarding overfitting patches via systematic co-exploration of the patch space and input space. We leverage concolic path exploration to systematically traverse the input space (and generate inputs), while ruling out significant parts of the patch space. Given a long enough time budget, this approach allows a significant reduction in the pool of patch candidates, as shown by our experiments. We implemented our technique in the form of a tool called 'CPR' and evaluated its efficacy in reducing the patch space by discarding overfitting patches from a pool of plausible patches. We evaluated our approach for fixing real-world software vulnerabilities and defects, for fixing functionality errors in programs drawn from SV-COMP benchmarks used in software verification, as well as for test-suite guided repair. In our experiments, we observed a patch space reduction due to our concolic exploration of up to 74% for fixing software vulnerabilities and up to 63% for SV-COMP programs. Our technique presents the viewpoint of gradual correctness - repair run over longer time leads to less overfitting fixes.

In this article, we introduce a probabilistic verification algorithm for stochastic regular expressions over a probabilistic extension of the Action based Computation Tree Logic (ACTL*). The main results include a novel model checking algorithm and a semantics on the probabilistic action logic for stochastic regular expressions (SREs). Specific to our model checking algorithm is that SREs are defined via local probabilistic functions. Such functions are beneficial since they enable to verify properties locally for sub-components. This ability provides a flexibility to reuse the local results for the global verification of the system; hence, the framework can be used for iterative verification. We demonstrate how to model a system with an SRE and how to verify it with the probabilistic action based logic and present a preliminary performance evaluation with respect to the execution time of the reachability algorithm.

Models in Model-driven Engineering are primary development artifacts that are heavily edited in all stages of software development and that can become temporarily inconsistent during editing. In general, there are many alternatives to resolve an inconsistency, and which one is the most suitable depends on a variety of factors. As also proposed by recent approaches to model repair, it is reasonable to leave the actual choice and approval of a repair alternative to the discretion of the developer. Model repair tools can support developers by proposing a list of the most promising repairs. Such repair recommendations will be only accepted in practice if the generated proposals are plausible and understandable, and if the set as a whole is manageable. Current approaches, which mostly focus on exhaustive search strategies, exploring all possible model repairs without considering the intention of historic changes, fail in meeting these requirements. In this article, we present a new approach to generate repair proposals that aims at inconsistencies that have been introduced by past incomplete edit steps that can be located in the version history of a model. Such an incomplete edit step is either undone or it is extended to a full execution of a consistency-preserving edit operation. The history-based analysis of inconsistencies as well as the generation of repair recommendations are fully automated, and all interactive selection steps are supported by our repair tool called R E V ISION . We evaluate our approach using histories of real-world models obtained from popular open-source modeling projects hosted in the Eclipse Git repository, including the evolution of the entire UML meta-model. Our experimental results confirm our hypothesis that most of the inconsistencies, namely, 93.4, can be resolved by complementing incomplete edits. 92.6% of the generated repair proposals are relevant in the sense that their effect can be observed in the models’ histories. 94.9% of the relevant repair proposals are ranked at the topmost position.

Detecting regression bugs in software evolution, analyzing side-channels in programs and evaluating robustness in deep neural networks (DNNs) can all be seen as instances of differential software analysis, where the goal is to generate diverging executions of program paths. Two executions are said to be diverging if the observable program behavior differs, e.g., in terms of program output, execution time, or (DNN) classification. The key challenge of differential software analysis is to simultaneously reason about multiple program paths, often across program variants.

Fuzzing or fuzz testing is an established technique that aims to discover unexpected program behavior (e.g., bugs, security vulnerabilities, or crashes) by feeding automatically generated data into a program under test. However, the application of fuzzing to test Model-Driven Software Engineering (MDSE) tools is still limited because of the difficulty of existing fuzzers to provide structured, well-typed inputs, namely models that conform to typing and consistency constraints induced by a given meta-model and underlying modeling framework. By drawing from recent advances on both fuzz testing and automated model generation, we present three different approaches for fuzzing MDSE tools: A graph grammar-based fuzzer and two variants of a coverage-guided mutation-based fuzzer working with different sets of model mutation operators. Our evaluation on a set of real-world MDSE tools shows that our approaches can outperform both standard fuzzers and model generators w.r.t. their fuzzing capabilities. Moreover, we found that each of our approaches comes with its own strengths and weaknesses in terms of fault finding capabilities and the ability to cover different aspects of the system under test. Thus the approaches complement each other, forming a fuzzer suite for testing MDSE tools.

Summary Pure spectrum‐based fault localization (SBFL) is a well‐studied statistical debugging technique that only takes a set of test cases (some failing and some passing) and their code coverage as input and produces a ranked list of suspicious program elements to help the developer identify the location of a bug that causes a failed test case. Studies show that pure SBFL techniques produce good ranked lists for small programs. However, our previous study based on the iBugs benchmark that uses the A spect J repository shows that, for realistic programs, the accuracy of the ranked list is not suitable for human developers. In this paper, we confirm this based on a combined empirical evaluation with the iBugs and the D efects4 J benchmark. Our experiments show that, on average, at most ∼40 % , ∼80 % , and ∼90 % of the bugs can be localized reliably within the first 10, 100, and 1000 ranked lines, respectively, in the D efects4 J benchmark. To reliably localize 90 % of the bugs with the best performing SBFL metric D ∗ , ∼450 lines have to be inspected by the developer. For human developers, this remains unsuitable, although the results improve compared with the results for the A spect J benchmark. Based on this study, we can clearly see the need to go beyond pure SBFL and take other information, such as information from the bug report or from version history of the code lines, into consideration.

Automated program repair has been studied via the use of techniques involving search, semantic analysis and artificial intelligence. Most of these techniques rely on tests as the correctness criteria, which causes the test overfitting problem. Although various approaches such as learning from code corpus have been proposed to address this problem, they are unable to guarantee that the generated patches generalize beyond the given tests. This work studies automated repair of errors using a reference implementation. The reference implementation is symbolically analyzed to automatically infer a specification of the intended behavior. This specification is then used to synthesize a patch that enforces conditional equivalence of the patched and the reference programs. The use of the reference implementation as an implicit correctness criterion alleviates overfitting in test-based repair. Besides, since we generate patches by semantic analysis, the reference program may have a substantially different implementation from the patched program, which distinguishes our approach from existing techniques for regression repair like Relifix. Our experiments in repairing the embedded Linux Busybox with GNU Coreutils as reference (and vice-versa) revealed that the proposed approach scales to real-world programs and enables the generation of more correct patches.

Complex software systems experience failures at runtime even though a lot of effort is put into the development and operation. Reactive approaches detect these failures after they have occurred and already caused serious consequences. In order to execute proactive actions, the goal of online failure prediction is to detect these failures in advance by monitoring the quality of service or the system events. Current failure prediction approaches look at the system or individual components as a monolith without considering the architecture of the system. They disregard the fact that the failure in one component can propagate through the system and cause problems in other components. In this paper, we propose a hierarchical online failure prediction approach, called Hora, which combines component failure predictors with architectural knowledge. The failure propagation is modeled using Bayesian networks which incorporate both prediction results and component dependencies extracted from the architectural models. Our approach is evaluated using Netflix’s server-side distributed RSS reader application to predict failures caused by three representative types of faults: memory leak, system overload, and sudden node crash. We compare Hora to a monolithic approach and the results show that our approach can improve the area under the ROC curve by 9.9%.

Automated test suite generation (ATSG) is an important topic in software engineering, with a wide range of techniques and tools being used in academia and industry. While their usefulness is widely recognized, due to the labor-intensive nature of the task, the effectiveness of the different techniques in automatically generating test cases for different software systems is not thoroughly understood. Despite many studies introducing various ATSG techniques, much remains to be learned, however, about what makes a particular technique work well (or not) for a specific software system. In this paper, we seek an answer to the question: “What features of a software system impact the effectiveness of ATSG techniques?” Once these features are identified, can they be used to select the most effective ATSG technique for a particular software system? To this end, we have implemented the mapping the effectiveness of test automation (META) tool, a new framework that identifies important software features that can be used to select suitable ATSG techniques to apply to new software systems. We evaluate the framework on a large set of open-source software projects and three ATSG techniques. The evaluation indicates that the number of methods in a class, the coupling between object classes, and the response for a class are the most indicative of what makes a software system hard to test by different techniques. The decision tree for ATSG technique selection generated by the META framework has an 88% accuracy, as shown by n-fold cross validation.

In the past, spectrum-based fault localization (SBFL) techniques have been developed to pinpoint a fault location in a program given a set of failing and successful test executions. Most of the algorithms use similarity coefficients and have only been evaluated on established but small benchmark programs from the Software-artifact Infrastructure Repository (SIR). In this paper, we evaluate the feasibility of applying 33 state-of-the-art SBFL techniques to a large real-world project, namely ASPECTJ. From an initial set of 350 faulty version from the iBugs repository of ASPECTJ we manually classified 88 bugs where SBFL techniques are suitable. Notably, only 11 bugs of these bugs can be found after examining the 1000 most suspicious lines and on average 250 source code files need to be inspected per bug. Based on these results, the study showcases the limitations of current SBFL techniques on a larger program.

Debugging is a costly process that consumes much of developer time and energy. To help reduce debugging effort, many studies have proposed various fault localization approaches. These approaches take as input a set of test cases (some failing, some passing) and produce a ranked list of program elements that are likely to be the root cause of the failures (i.e., failing test cases). In this work, we propose Savant, a new fault localization approach that employs a learning-to-rank strategy, using likely invariant diffs and suspiciousness scores as features, to rank methods based on their likelihood to be a root cause of a failure. Savant has four steps: method clustering & test case selection, invariant mining, feature extraction, and method ranking. At the end of these four steps, Savant produces a short ranked list of potentially buggy methods. We have evaluated Savant on 357 real-life bugs from 5 programs from the Defects4J benchmark. Out of these bugs, averaging over 100 repeated trials with different seeds to randomly break ties, we find that on average Savant can identify correct buggy methods for 63.03, 101.72, and 122 bugs at top 1, 3, and 5 positions in the ranked lists that Savant produces. We have compared Savant against several state-of-the-art fault localization baselines that work on program spectra. We show that Savant can successfully locate 57.73%, 56.69%, and 43.13% more bugs at top 1, top 3, and top 5 positions than the best performing baseline, respectively.

Adaptive software systems are designed to cope with unpredictable and evolving usage behaviors and environmental conditions. For these systems reasoning mechanisms are needed to drive evolution, which are usually based on models capturing relevant aspects of the running software. The continuous update of these models in evolving environments requires efficient learning procedures, having low overhead and being robust to changes. Most of the available approaches achieve one of these goals at the price of the other. In this paper we propose a lightweight adaptive filter to accurately learn time-varying transition probabilities of discrete time Markov models, which provides robustness to noise and fast adaptation to changes with a very low overhead. A formal stability, unbiasedness and consistency assessment of the learning approach is provided, as well as an experimental comparison with state-of-the-art alternatives.

Formal methods offer an effective means to assert the correctness of software systems through mathematical reasoning. However, the need to formulate system properties in a purely mathematical fashion can create pragmatic barriers to the application of these techniques. For this reason, Dwyer et al. invented property specification patterns which is a system of recurring solutions to deal with the temporal intricacies that would make the construction of reactive systems very hard otherwise. Today, property specification patterns provide general rules that help practitioners to qualify order and occurrence, to quantify time bounds, and to express probabilities of events. Nevertheless, a comprehensive framework combining qualitative, real-time, and probabilistic property specification patterns has remained elusive. The benefits of such a framework are twofold. First, it would remove the distinction between qualitative and quantitative aspects of events; and second, it would provide a structure to systematically discover new property specification patterns. In this paper, we report on such a framework and present a unified catalogue that combines all known plus 40 newly identified or extended patterns. We also offer a natural language front-end to map patterns to a temporal logic of choice. To demonstrate the virtue of this new framework, we applied it to a variety of industrial requirements, and use PSPWizard, a tool specifically developed to work with our unified pattern catalogue, to automatically render concrete instances of property specification patterns to formulae of an underlying temporal logic of choice.

All commonly used stochastic optimisation algorithms have to be parameterised to perform effectively. Adaptive parameter control (APC) is an effective method used for this purpose. APC repeatedly adjusts parameter values during the optimisation process for optimal algorithm performance. The assignment of parameter values for a given iteration is based on previously measured performance. In recent research, time series prediction has been proposed as a method of projecting the probabilities to use for parameter value selection. In this work, we examine the suitability of a variety of prediction methods for the projection of future parameter performance based on previous data. All considered prediction methods have assumptions the time series data has to conform to for the prediction method to provide accurate projections. Looking specifically at parameters of evolutionary algorithms (EAs), we find that all standard EA parameters with the exception of population size conform largely to the assumptions made by the considered prediction methods. Evaluating the performance of these prediction methods, we find that linear regression provides the best results by a very small and statistically insignificant margin. Regardless of the prediction method, predictive parameter control outperforms state of the art parameter control methods when the performance data adheres to the assumptions made by the prediction method. When a parameter's performance data does not adhere to the assumptions made by the forecasting method, the use of prediction does not have a notable adverse impact on the algorithm's performance.

Complex model transformation is crucial in several domains, including Model-Driven Engineering (MDE), information visualisation and data mapping. Most current approaches use meta-model-driven transformation specification via coding in textual scripting languages. This paper demonstrates a novel approach and tool support that instead provides for specification of correspondences between models using concrete visualisations of source and target models, and generates transformation scripts from these by-example model correspondence specifications.

Due to significant industrial demands toward software systems with increasing complexity and challenging quality requirements, software architecture design has become an important development activity and the research domain is rapidly evolving. In the last decades, software architecture optimization methods, which aim to automate the search for an optimal architecture design with respect to a (set of) quality attribute(s), have proliferated. However, the reported results are fragmented over different research communities, multiple system domains, and multiple quality attributes. To integrate the existing research results, we have performed a systematic literature review and analyzed the results of 188 research papers from the different research communities. Based on this survey, a taxonomy has been created which is used to classify the existing research. Furthermore, the systematic analysis of the research literature provided in this review aims to help the research community in consolidating the existing research efforts and deriving a research agenda for future developments.

Availability of several web services having a similar functionality has led to using quality of service (QoS) attributes to support services selection and management. To improve these operations and be performed proactively, time series ARIMA models have been used to forecast the future QoS values. However, the problem is that in this extremely dynamic context the observed QoS measures are characterized by a high volatility and time-varying variation to the extent that existing ARIMA models cannot guarantee accurate QoS forecasting where these models are based on a homogeneity (constant variation over time) assumption, which can introduce critical problems such as proactively selecting a wrong service and triggering unrequired adaptations and thus leading to follow-up failures and increased costs. To address this limitation, we propose a forecasting approach that integrates ARIMA and GARCH models to be able to capture the QoS attributes' volatility and provide accurate forecasts. Using QoS datasets of real-world web services we evaluate the accuracy and performance aspects of the proposed approach. Results show that the proposed approach outperforms the popular existing ARIMA models and improves the forecasting accuracy of QoS measures and violations by on average 28.7% and 15.3% respectively.

Predicting future values of Quality of Service (QoS) attributes can assist in the control of software intensive systems by preventing QoS violations before they happen. Currently, many approaches prefer Autoregressive Integrated Moving Average (ARIMA) models for this task, and assume the QoS attributes' behavior can be linearly modeled. However, the analysis of real QoS datasets shows that they are characterized by a highly dynamic and mostly nonlinear behavior to the extent that existing ARIMA models cannot guarantee accurate QoS forecasting, which can introduce crucial problems such as proactively triggering unrequired adaptations and thus leading to follow-up failures and increased costs. To address this limitation, we propose an automated forecasting approach that integrates linear and nonlinear time series models and automatically, without human intervention, selects and constructs the best suitable forecasting model to fit the QoS attributes' dynamic behavior. Using real-world QoS datasets of 800 web services we evaluate the applicability, accuracy, and performance aspects of the proposed approach, and results show that the approach outperforms the popular existing ARIMA models and improves the forecasting accuracy by on average 35.4%.

Currently software systems operate in highly dynamic contexts, and consequently they have to adapt their behavior in response to changes in their contexts or/and requirements. Existing approaches trigger adaptations after detecting violations in quality of service (QoS) requirements by just comparing observed QoS values to predefined thresholds without any statistical confidence or certainty. These threshold-based adaptation approaches may perform unnecessary adaptations, which can lead to severe shortcomings such as follow-up failures or increased costs. In this paper we introduce a statistical approach based on CUSUM control charts called AuDeQAV - Automated Detection of QoS Attributes Violations. This approach estimates at runtime a current status of the running system, and monitors its QoS attributes and provides early detection of violations in its requirements with a defined level of confidence. This enables timely intervention preventing undesired consequences from the violation or from inappropriate remediation. We validated our approach using a series of experiments and response time datasets from real-world web services.

Model checking provides a powerful means to assert and verify desired system properties. But, for the verification process to become feasible, a correct formulation of these properties in a temporal logic is necessary - a potential barrier to application in practice. Research on property specification has supplied us with rich pattern catalogs that capture commonly occurring system properties in different temporal logics. Furthermore, these property specification pattern catalogs usually offer both a structured English grammar to facilitate the pattern selection and an associated template solutions to express the properties formally. Yet, the actual use of property specification patterns remains cumbersome, due to limited tool support. For this reason, we have developed the Property Specification Pattern Wizard (PSPWizard), a framework that defines an interface for the currently accepted property specification pattern libraries. PSPWizard consists of two main building blocks: a mapping generator that weaves a given pattern library with a target logic and a GUI front-end to the structured English grammar tailored to those patterns that are supported in the target logic.

Abstract Failure Modes and Effects Analysis (FMEA) is a widely used system and software safety analysis technique that systematically identifies failure modes of system components and explores whether these failure modes might lead to potential hazards. In practice, FMEA is typically a labor‐intensive team‐based exercise, with little tool support. This article presents our experience with automating parts of the FMEA process, using a model checker to automate the search for system‐level consequences of component failures. The idea is to inject runtime faults into a model based on the system specification and check if the resulting model violates safety requirements, specified as temporal logical formulas. This enables the safety engineer to identify if a component failure, or combination of multiple failures, can lead to a specified hazard condition. If so, the model checker produces an example of the events leading up to the hazard occurrence which the analyst can use to identify the relevant failure propagation pathways and co‐effectors. The process is applied on three medium‐sized case studies modeled with Behavior Trees. Performance metrics for SAL model checking are presented. Copyright © 2011 John Wiley & Sons, Ltd.

Abstract Run‐time monitoring is an important technique to detect erroneous run‐time behaviors. Several techniques have been proposed to automatically generate monitors from specification languages to check temporal and real‐time properties. However, monitoring of probabilistic properties still requires manual generation. To overcome this problem, we define a formal property specification language called Probabilistic Timed Property Sequence Chart (PTPSC). PTPSC is a probabilistic and timed extension of the existing scenario‐based specification formalism Property Sequence Chart (PSC). We have defined a formal grammar‐based syntax and have implemented a syntax‐directed translator that can automatically generate a probabilistic monitor which combines timed B”uchi automata and a sequential statistical hypothesis test process. We validate the generated monitors with a set of experiments performed with our tool WS‐PSC Monitor. Copyright © 2011 John Wiley & Sons, Ltd.

Service-based systems that are dynamically composed at runtime to provide complex, adaptive functionality are currently one of the main development paradigms in software engineering. However, the Quality of Service (QoS) delivered by these systems remains an important concern, and needs to be managed in an equally adaptive and predictable way. To address this need, we introduce a novel, tool-supported framework for the development of adaptive service-based systems called QoSMOS (QoS Management and Optimization of Service-based systems). QoSMOS can be used to develop service-based systems that achieve their QoS requirements through dynamically adapting to changes in the system state, environment, and workload. QoSMOS service-based systems translate high-level QoS requirements specified by their administrators into probabilistic temporal logic formulae, which are then formally and automatically analyzed to identify and enforce optimal system configurations. The QoSMOS self-adaptation mechanism can handle reliability and performance-related QoS requirements, and can be integrated into newly developed solutions or legacy systems. The effectiveness and scalability of the approach are validated using simulations and a set of experiments based on an implementation of an adaptive service-based system for remote medical assistance.

Nowadays requirements related to quality attributes such as performance, reliability, safety and security are often considered the most important requirements for software development projects. To reason about these quality attributes different stochastic models can be used. These models enable probabilistic verification as well as quantitative prediction at design time. On the other hand, these models could be also used to perform runtime adaptation in order to achieve certain quality goals. This workshop aims to provide a forum for researchers in these areas that should help with the adoption of quantitative stochastic models into general software development processes.

Probabilistic models are widely used in Architecture-based reliability prediction in software intensive systems. However, for most of the cases, it is computationally expensive to compute the reliability metrics and re-compute them once the system has evolved or is used in a different environment. In this paper, we introduce an efficient computation method for Discrete Time Markov Chain based abstractions, which computes reliability metrics once, and we provide an incremental technique to recompute these metrics in case of a single change in the reliability evaluation model. As a result, fast an efficient reliability computation can be provided for scenarios like design-time architecture optimization and run time adaptation. An experimental validation of the new method shows a significant improvement in terms of computation time required to re-evaluate an evolved architecture.

Abstract Components in programmable systems often exhibit patterns of failure that are independent of function or system context. In this paper, we show that it is possible to capture, and reuse where appropriate, such patterns for the purposes of system safety analysis. We describe a language that enables abstract specification of failure behaviour and define the syntax and semantics of this language. The language extends concepts originally defined in HiP‐HOPS, a technique that enables a largely automated form of compositional system safety analysis. The paper describes how this language can be used to describe component failure patterns and demonstrates how it can be applied using a simple fuel system example. The approach is evaluated on a set of retrospective industrial case studies, where data‐mining and reverse engineering techniques are applied in order to identify hidden patterns in legacy safety analyses. Results show clear potential for practical use of patterns in HiP‐HOPS. We argue that careful specification and reuse of failure patterns in conjunction with a tool that automates Fault Tree and Failure Modes and Effects Analysis can help to simplify complex safety assessments. Copyright © 2010 John Wiley & Sons, Ltd.

Decisions regarding the mapping of software components to hardware nodes affect the quality of the resulting system. Making these decisions is hard when considering the ever-growing complexity of the search space, as well as conflicting objectives and constraints. An automation of the solution space exploration would help not only to make better decisions but also to reduce the time of this process. In this paper, we propose to employ Ant Colony Optmisation (ACO) as a multi-objective optimisation strategy. The constructive approach is compared to an iterative optimisation procedure - a Genetic Algorithm (GA) adaptation - and was observed to perform suprisingly similar, although not quite on a par with the GA, when validated based on a series of experiments.

Probabilistic properties are considered as the most important requirements for a variety of software systems, since they are used to formulate extra-functional requirements such as reliability, availability, safety, security and performance requirements. Currently, several probabilistic logics have been proposed to specify such important properties. However, due to the inherent complexity of the underlying temporal logics, these probabilistic logics are rather complex and software developers have problems using them to correctly specify the intended properties. To overcome this problem, we define a formal and graphical property specification language called probabilistic timed property sequence charts (PTPSC) which is a probabilistic extension of property sequence charts (PSC). We illustrate the use of PTPSC in the context of a vehicle-to-vehicle communication device for avoiding traffic accidents.

Monitoring allows for checking if a system fulfils its requirements at runtime. This is required for quality assurance purposes. Currently several approaches exist to monitor standard and timing properties. However, a current challenge is to provide a comprehensive approach for monitoring probabilistic properties, as they are used to formulate performance, reliability, safety, and availability requirements. The main problem of these probabilistic properties is that there is no binary acceptance condition. To overcome this problem, this paper describes a monitoring approach called ProMo that is based on acceptance sampling and sequential hypothesis testing. This approach is validated based on several experiments that have been performed on an example system which provides medical assistance in remote areas.

Probabilistic verification techniques are a powerful means to ensure that a software-intensive system fulfills its quality requirements. To apply these techniques an accurate specification of the required properties in a probabilistic temporal logic is necessary. To help practitioners formulate these properties correctly, this paper presents a specification pattern system of common probabilistic properties called ProProST. This pattern system has been a developed based on a survey of 152 properties from academic examples and 48 properties of real-word quality requirements from avionic, defence and automotive systems. Furthermore, a structured English grammar that can guide in the specification of probabilistic properties is given. Similar to previous specification patterns for traditional and real-time properties, the presented specification pattern system and the structured English grammar captures expert knowledge and helps practitioners to correctly apply formal verification techniques.

Architecture trade-off analysis methods are appropriate techniques to evaluate design decisions and design alternatives with respect to conflicting quality requirements. However, the identification of good design alternatives is a time consuming task, which is currently performed manually. To automate this task, this paper proposes to use evolutionary algorithms and multi-objective optimization strategies based on architecture refactorings to identify a sufficient set of design alternatives. This approach will reduce development costs and improve the quality of the final system, because an automated and systematic search will identify more and better design alternatives.

Architectural refactorings are an appropriate technique for the development and improvement of architectural specifications. However, these refactorings are often applied manually. This paper presents a mapping of an architectural specification language to a hypergraph-based data structure. Thus, architectural refactorings can be formalized as hypergraph transformation rules and can be applied automatically.