Software systems with large parameter spaces, nondeterminism and high computational cost are challenging to test. Recently, software testing techniques based on causal inference have been successfully applied to systems that exhibit such characteristics, including scientific models and autonomous driving systems. One significant limitation is that these are restricted to test properties where all of the variables involved can be observed and where there are no interactions between variables. In practice, this is rarely guaranteed; the logging infrastructure may not be available to record all of the necessary runtime variable values, and it can often be the case that an output of the system can be affected by complex interactions between variables. To address this, we leverage two additional concepts from causal inference, namely effect modification and instrumental variable methods. We build these concepts into an existing causal testing tool and conduct an evaluative case study which uses the concepts to test three system-level requirements of CARLA, a high-fidelity driving simulator widely used in autonomous vehicle development and testing. The results show that we can obtain reliable test outcomes without requiring large amounts of highly controlled test data or instrumentation of the code, even when variables interact with each other and are not recorded in the test data.

Causal reasoning is becoming an increasingly popular technique for testing software. In this setting, the tester starts from a simple directed graph that captures their underlying understanding of causal relationships between relevant variables in the program, and this knowledge is then used to reason about causal input-output relationships that are observed during testing. One question that has not yet been addressed in this context is how to measure test adequacy: How do we know whether a causal relationship (or set of relationships) has been properly established by a test set? In this paper we present a metric inspired by Weyuker's notion of inference adequacy. For a given causal relationship, we estimate the causal effect from the test data. The basis of our adequacy metric is then an estimate of the convergence of this estimate, which we calculate using statistical bootstrapping. We evaluate our metric on tests for three diverse computational models. The results show a statistically significant correlation between our metric and a test suite's ability to detect mutants, and also that it is a good indicator of whether a sufficient number of system executions have been observed to trust the outcome of the test.

From simulating galaxy formation to viral transmission in a pandemic, scientific models play a pivotal role in developing scientific theories and supporting government policy decisions that affect us all. Given these critical applications, a poor modelling assumption or bug could have far-reaching consequences. However, scientific models possess several properties that make them notoriously difficult to test, including a complex input space, long execution times, and non-determinism, rendering existing testing techniques impractical. In fields such as epidemiology, where researchers seek answers to challenging causal questions, a statistical methodology known as Causal inference has addressed similar problems, enabling the inference of causal conclusions from noisy, biased, and sparse data instead of costly experiments. This article introduces the causal testing framework: a framework that uses causal inference techniques to establish causal effects from existing data, enabling users to conduct software testing activities concerning the effect of a change, such as metamorphic testing, a posteriori . We present three case studies covering real-world scientific models, demonstrating how the causal testing framework can infer metamorphic test outcomes from reused, confounded test data to provide an efficient solution for testing scientific modelling software.

Metamorphic testing provides a means by which to generate succinct test oracles that can apply to large input spaces. For this it depends on the formulation of metamorphic relations, which generally require extensive domain expertise and human input. To address this problem, we present a model-based testing approach that can automatically generate metamorphic relations and associated tests. Our approach is motivated by the observation that metamorphic testing is a fundamentally causal task. We show how it is possible to leverage lightweight graph-based modelling techniques from the field of causal inference to specify causal properties of the system-under-test. Through a series of controlled experiments, we find that the proposed approach is robust to misspecification and can test evasive causal relationships (i.e. those that are difficult to exercise and observe) when combined with an appropriate test generation strategy. We also apply the approach to two case studies from the Defects4J framework with known bugs that affect causal behaviour. The results of these case studies suggest that the approach is not only useful for catching bugs affecting causal structure, but also alerting the user to inaccuracies in the specification.

Abstract Model checkers and interactive proof assistants are both used in the assurance of critical systems. Where theorem proving involves the use of axioms and inference rules to mathematically prove defined properties, model checkers can be used to provide concrete counterexamples to refute them. Thus, the two techniques can be thought of as complementary, and it is helpful to use both in tandem to take advantage of their respective strengths. However, this requires us to translate our system model and our desired properties between the two tools which is a time-consuming and error prone process if done manually. The key contribution of this work is a set of automated tools to translate between the Isabelle/HOL proof assistant and the Symbolic Analysis Laboratory (SAL) model checker. We focus on systems specified as extended finite state machines (EFSMs) and on properties specified in linear temporal logic (LTL). We present our representations in the two tools and demonstrate the applicability of our system with respect to an academic example and two realistic case studies. This is a significant contribution to broadening the applicability of these formal approaches, since it allows two powerful verification tools to be easily used in tandem without the risk of human error.

Evolutionary algorithms (EAs) come in all shapes and sizes. Theoretical investigations focus on simple, bare-bones EAs while applications often use more sophisticated EAs that perform well on the problem at hand. What is often unclear is whether a large degree of algorithm sophistication is necessary, and if so, how much performance is gained by adding complexity to an EA. We address this question by comparing the performance of a wide range of theory-driven EAs, from bare-bones algorithms like the (1+1) EA, a (2+1) GA and simple population-based algorithms to more sophisticated ones like the (1+(λ,λ)) GA and algorithms using fast (heavy-tailed) mutation operators, against sophisticated and highly effective EAs from specific applications. This includes a famous and highly cited Genetic Algorithm for the Multidimensional Knapsack Problem and the Parameterless Population Pyramid for Ising Spin Glasses and MaxSat. While for the Multidimensional Knapsack Problem the sophisticated algorithm performs best, surprisingly, for large Ising and MaxSat instances the simplest algorithm performs best. We also derive conclusions about the usefulness of populations, crossover and fast mutation operators. Empirical results are supported by statistical tests and contrasted against theoretical work in an attempt to link theoretical and empirical results on EAs.