Abstract Context The use of automated driving systems (ADSs) in the real world requires rigorous testing to ensure safety. To increase trust, ADSs should be tested on a large set of diverse road scenarios. Literature suggests that if a vehicle is driven along a set of geometrically diverse roads—measured using various diversity measures (DMs)—it will react in a wide range of behaviours, thereby increasing the chances of observing failures, or strengthening the confidence in its safety, if no failures are observed. However, this assumption has never been tested before, nor have road DMs been assessed for their properties. Objective Our goal was to perform an exploratory study on 53 currently used and new, potentially promising road DMs. Specifically, our research questions looked into the road DMs themselves, to analyse their properties (e.g. monotonicity , computation efficiency ), and to test correlation between DMs. Furthermore, we investigated the use of road DMs to determine whether the assumption that diverse test suites of roads expose diverse driving behaviour holds. Method Our empirical analysis relies on a state-of-the-art, open-source ADS testing infrastructure and uses a data set containing over 97,000 individual road geometries and matching simulation data that were collected using two driving agents. By considering test suites of various sizes and measuring their roads’ geometric diversity, we studied road DM properties, the correlation between road DMs, and the correlation between road DMs and the observed behaviour. Results Our findings reveal a strong correlation between road diversity and behavioural diversity, confirming that geometrically diverse test suites systematically exercise diverse driving behaviours. We identified and aggregations as most effective, with achieving the strongest correlation of 0.95 while requiring minimal computation time. The analysed measures maintain robust correlation with behavioural diversity across test suites containing roads of varying lengths, eliminating the need for length normalisation. Conclusions These results empirically validate the fundamental assumption underlying diversity-driven ADS testing: road geometry diversity serves as a reliable proxy for behavioural diversity. For practitioners, we recommend or as optimal choices, whilst -based measures should be avoided entirely. The near-identical correlation patterns observed across architecturally different driving agents indicate that our findings generalise beyond specific ADS implementations, providing a solid foundation for diversity-driven test generation and selection.

The overtake car maneuver involves high risk and complex judgement. For autonomous vehicles this is challenging, especially for human-initiated overtake requests. If a user requests the maneuver there must be a rapid safety assessment. Language models have great potential to classify safety with explanations, but they struggle to disentangle critical information from complex vehicular environments. We apply CLEAR (Cue Learning using Evolution for Accurate Recognition) to evolve prompt cues that optimize the ability of language models to correctly predict safety scores for overtaking maneuvers. To achieve this, we create a novel open-source symbolic traffic model EvoDrive designed specifically for EC research, which outputs LLM-readable snapshots. We show that LLMs + EvoDrive with CLEAR can reduce error by more than 20% compared to without CLEAR, with statistically significant results. Analysis shows evolved cues are coherent and have reduced variability in LLM output.

This paper presents a multimodal human-robot interaction (HRI) system for educational contexts implemented on the humanoid robot Pepper. The system leverages multiple communicative channels, allowing learners to combine speech with tablet interaction while the robot responds through synchronized speech, textual captions and dynamic visual cues. To ensure robustness and reliability, we introduce the use of Metamorphic Testing for multimodal HRI. By validating system behavior through systematic input transformations, we demonstrate how metamorphic testing can uncover inconsistencies across linguistic, visual and cross-modal interactions. This work contributes both a novel methodological framework for evaluating multimodal HRI systems and an application to educational robotics.

Autonomous driving systems (ADSs) must be sufficiently tested to ensure their safety. Though various ADS testing methods have shown promising results, they are limited to a fixed vehicle characteristics setting (VCS). The impact of variations in vehicle characteristics (e.g., mass, tire friction) on the safety of ADSs has not been sufficiently and systematically studied. Such variations are often due to wear and tear, production errors and so on, which may lead to unexpected driving behaviours of ADSs. To this end, in this article, we propose a method, named SafeVar , to systematically find minimum variations to the original vehicle characteristics setting, which affect the safety of the ADS deployed on the vehicle. To evaluate the effectiveness of SafeVar , we employed two ADSs and conducted experiments with two driving scenarios. Results show that SafeVar , equipped with NSGA-II, generates more critical settings that put the vehicle into unsafe situations, as compared with the baseline algorithm. We also identified critical vehicle characteristics and reported to which extent varying their settings put the ADS vehicle into unsafe situations.

With the rapid advancement of quantum computing, research on quantum machine learning (QML) algorithms has grown significantly. Among these, the Quantum Neural Network (QNN) stands out as one of the promising algorithms that integrates the principles of quantum computing with artificial neural networks to process data. Inspired by applications of QNN across fields, we investigate their use in software testing for the Cancer Registry of Norway (CRN), part of the Norwegian Institute of Public Health (NIPH), responsible for cancer statistics among the Norwegian population. CRN develops a complex socio-technical software system, Cancer Registration Support System ( \(\mathtt{CaReSS}\) ), interacting with many entities (e.g., hospitals, medical laboratories, and other patient registries) to achieve its task. For cost-effective testing of \(\mathtt{CaReSS}\) , CRN has employed \(\mathtt{EvoMaster}\) , an AI-based REST API testing tool combined with an integrated classical machine learning model \(\mathtt{EvoClass}\) . Within this context, we propose \(\mathtt{EvoQlass}\) to investigate the feasibility of using, inside \(\mathtt{EvoMaster}\) , a QNN classifier, instead of the existing classical machine learning model. Results indicate that \(\mathtt{EvoQlass}\) can achieve performance comparable to that of \(\mathtt{EvoClass}\) . We further explore the effects of various QNN configurations on performance and offer recommendations for optimal QNN settings for future QNN developers.

Self-adaptation in maritime autonomous vessels (AVs) enables them to adapt their behaviors to address unexpected situations while maintaining dependability requirements. During the design of such AVs, it is crucial to understand and identify the settings that should trigger adaptations, enabling validation of their implementation. To this end, we focus on the navigation software of AVs, which must adapt their behavior during operation through adaptations. AVs often rely on predefined waypoints to guide them along designated routes, ensuring safe navigation. We propose a multi-objective search-based approach, called WPgen, to generate minor modifications to the predefined set of waypoints, keeping them as close as possible to the original waypoints, while causing the AV to navigate inappropriately when navigating with the generated waypoints. WPgen uses NSGA-II as the multi-objective search algorithm with three seeding strategies for its initial population, resulting in three variations of WPgen. We evaluated these variations on three AVs (one overwater tanker and two underwater). We compared the three variations of WPgen with Random Search as the baseline and with each other. Experimental results showed that the effectiveness of these variations varied depending on the AV. Based on the results, we present the research and practical implications of WPgen.

DETOUR is a test case selector of road tests for self-driving cars, that participated to the “ICST Tool Competition 2025 - Self-Driving Car Testing Track”. DETOUR first transforms road tests, from the provided Cartesian representation, to a curvature representation based on the Frenet frame. Then, DETOUR follows a two-step process. In the first step, tests are clustered according to their similarity; this step considers both tests that have been previously executed (for which it is known whether they pass or fail) and tests that have not been executed. Then, in the second step, the tool selects, from the obtained clusters, the non-executed tests that are closer to executed tests that are known to be failing.

PALM is a generator of scenarios for UAV testing, that participated in the ICST Tool Competition 2025 - CPS-UAV Test Case Generation Track. PALM adopts Monte Carlo Tree Search (MCTS) to search for different placements of obstacles of different sizes in the mission environment. By increasing the tree depth, a new obstacle is added to the environment; instead, by adding a new node in the current tree level, the tool optimises the placement and the dimension of the last added obstacle.

Autonomous Vehicles (AVs) must be thoroughly tested to meet high safety requirements. Scenario-based testing using simulation is a common approach for validating them. Usually, scenarios test only one ego vehicle against road users with pre-defined behaviors called Non-Playable Characters (NPC). Such scenarios ensure reproducibility but are not always relevant and realistic, as they do not capture interactions between (e.g., non-cooperative) AVs. Consequently, they are unsuitable for testing safety-critical emerging behaviors like those happening in the real world. To tackle this problem, we propose TIAV, an approach for generating interactive critical scenarios that allows developers to study how AVs influence each other. Experiments on the reference CommonRoad simulation framework show that TIAV can identify scenarios leading to collisions and disengagements and trigger significantly more failures than a random baseline. Thanks to its ability to expose unsafe AV interactions, TIAV allows developers to validate AVs' functional correctness and check the effects of AVs' simultaneous deployment. TIAV is available as open-source software: https://github.comJparcaini/TIAV

Robots are increasingly becoming part of our daily lives, interacting with both the environment and humans to perform their tasks. The software of such robots often undergoes upgrades, for example, to add new functionalities, fix bugs, or delete obsolete functionalities. As a result, regression testing of robot software becomes necessary. However, determining the expected correct behavior of robots (i.e., a test oracle) is challenging due to the potentially unknown environments in which the robots must operate. To address this challenge, machine learning (ML)-based test oracles present a viable solution. This paper reports on the development of a test oracle to support regression testing of autonomous mobile robots built by PAL Robotics (Spain), using quantum machine learning (QML), which enables faster training and the construction of more precise test oracles. Specifically, we propose a hybrid framework, QuReBot, that combines both quantum reservoir computing (QRC) and a simple neural network, inspired by residual connection, to predict the expected behavior of a robot. Results show that QRC alone fails to converge in our case, yielding high prediction error. In contrast, QuReBot converges and achieves 15% reduction of prediction error compared to the classical neural network baseline. Finally, we further examine QuReBot under different configurations and offer practical guidance on optimal settings to support future robot software testing.

Deep Neural Networks (DNNs) have become a core component in several safety-critical tasks like Autonomous Driving. To ensure their safe usage in these scenarios, DNN repair approaches have been used to fix erroneous predictions by changing the values of a small subset of parameters like model weights. However, in order to work effectively, these approaches require the presence of categorical outputs, for which it is possible to provide a clear assessment of correctness. Therefore, they do not work well for regression networks for which such binary assessment is not possible. To solve this issue, we propose a new approach, called Semsegrep, to enable practitioners to repair regression networks like semantic segmentation, which are increasingly deployed in these safety-critical domains. Semseg-repfirst selects weights that contribute to erroneous predictions, consequently decreasing a target metric like Mean Intersection over Union. It then employs a filtering method that selects a subset of these weights based on their determined potential for repairing the model. Lastly, it uses a search-based repair approach to generate a patch with new value assignments for the selected weights. Experiments conducted on a semantic segmentation model and four datasets provided by our industry partner show that Semsegrep is able to improve the model according to the given target metric without affecting the overall accuracy, and it is better than a state-of-the-art repair approach.

Abstract As a new research area, quantum software testing lacks systematic testing benchmarks to assess testing techniques’ effectiveness. Recently, some open-source benchmarks and mutation analysis tools have emerged. However, there is insufficient evidence on how various quantum circuit characteristics (e.g., circuit depth, number of quantum gates), algorithms (e.g., Quantum Approximate Optimization Algorithm), and mutation characteristics (e.g., mutation operators) affect the detection of mutants in quantum circuits. Studying such relations is important to systematically design faulty benchmarks with varied attributes (e.g., the difficulty in detecting a seeded fault) to facilitate assessing the cost-effectiveness of quantum software testing techniques efficiently. To this end, we present a large-scale empirical evaluation with more than 700K faulty benchmarks (quantum circuits) generated by mutating 382 real-world quantum circuits. Based on the results, we provide valuable insights for researchers to define systematic quantum mutation analysis techniques. We also provide a tool to recommend mutants to users based on chosen characteristics (e.g., a quantum algorithm type) and the required difficulty of detecting mutants. Finally, we also provide faulty benchmarks that can already be used to assess the cost-effectiveness of quantum software testing techniques.

Falsification, whose aim is to detect unsafe behaviors of cyber-physical systems (CPS) that violate signal temporal logic (STL) specifications, has been actively investigated in the past decade. Although numerous falsification approaches have been proposed, the falsification community suffers from a shortage of benchmarks that hinders a thorough assessment of those falsification approaches. In this article, we bridge this gap by proposing an automated approach for generating falsification benchmarks. Our approach is data-driven: first, we generate different time-variant traces (acting as system output traces) that satisfy a given STL specification, and we associate these with corresponding system input traces; then, we use these input and output traces to train an LSTM model that generalizes them. These models can serve as benchmarks for assessing falsification approaches against the given specification. In the experimental evaluation, we validate the generated models by measuring their ability to differentiate the performance of different falsification approaches. Our generated models expose strengths and weaknesses of all the considered falsification approaches, which was not achieved by benchmarks currently used in the falsification community. These results demonstrate the usefulness of our approach and can potentially push forward subsequent research in falsification.

Cyber-physical systems (CPSs) are increasingly adopting deep neural networks (DNNs) as controllers, giving birth to AI-enabled CPSs . Despite their advantages, many concerns arise about the safety of DNN controllers. Numerous efforts have been made to detect system executions that violate safety specifications; however, once a violation is detected, to fix the issue, it is necessary to localise the parameters of the DNN controller responsible for the wrong decisions leading to the violation. This is particularly challenging, as it requires to consider a sequence of control decisions, rather than a single one, preceding the violation. To tackle this problem, we propose SpectAcle , that can localise the faulty parameters in DNN controllers. SpectAcle considers the DNN inferences preceding the specification violation and uses forward impact to determine the DNN parameters that are more relevant to the DNN outputs. Then, it identifies which of these parameters are responsible for the specification violation, by adapting classic suspiciousness metrics. Moreover, we propose two versions of SpectAcle , that consider differently the timestamps that precede the specification violation. We experimentally evaluate the effectiveness of SpectAcle on 6,067 faulty benchmarks, spanning over different application domains. The results show that SpectAcle can detect most of the faults.

As quantum computers advance, the complexity of the software they can execute increases as well. To ensure this software is efficient, maintainable, reusable, and cost-effective—key qualities of any industry-grade software—mature software engineering practices must be applied throughout its design, development, and operation. However, the significant differences between classical and quantum software make it challenging to directly apply classical software engineering methods to quantum systems. This challenge has led to the emergence of Quantum Software Engineering (QSE) as a distinct field within the broader software engineering landscape. In this work, a group of active researchers analyze in depth the current state of QSE research. From this analysis, the key areas of QSE are identified and explored in order to determine the most relevant open challenges that should be addressed in the next years. These challenges help identify necessary breakthroughs and future research directions for advancing QSE.

Quantum annealers are specialized quantum computers for solving combinatorial optimization problems with special quantum computing characteristics, e.g., superposition and entanglement. Theoretically, quantum annealers can outperform classic computers. However, current quantum annealers are constrained by a limited number of qubits and cannot demonstrate quantum advantages. Nonetheless, research is needed to develop novel mechanisms to formulate combinatorial optimization problems for quantum annealing (QA). However, QA applications in software engineering remain unexplored. Thus, we propose BootQA , the very first effort at solving test case minimization (TCM) problems on classical software with QA. We provide a novel TCM formulation for QA and utilize bootstrap sampling to optimize the qubit usage. We also implemented our TCM formulation in three other optimization processes: simulated annealing (SA), QA without problem decomposition, and QA with an existing D-Wave problem decomposition strategy, and conducted an empirical evaluation with three real-world TCM datasets. Results show that BootQA outperforms QA without problem decomposition and QA with the existing decomposition strategy regarding effectiveness. Moreover, BootQA ’s effectiveness is similar to SA. Finally, BootQA has higher efficiency in terms of time when solving large TCM problems than the other three optimization processes.

Abstract In this paper, we present a tool for monitoring the traces of cyber-physical systems (CPS) at runtime, with respect to Signal Temporal Logic (STL) specifications. Our tool is based on the recent advances of causation monitoring, which reports not only whether an executing trace violates the specification, but also how relevant the increment of the trace at each instant is to the specification violation. In this way, it can deliver more information about system evolution than classic online robust monitors. Moreover, by adapting two dynamic programming strategies, our implementation significantly improves the efficiency of causation monitoring, allowing its deployment in practice. The tool is implemented as a executable and can be easily adapted to monitor CPS in different formalisms. We evaluate the efficiency of the proposed monitoring tool, and demonstrate its superiority over existing robust monitors in terms of the information it can deliver about system evolution.

In AI-enabled CPSs, DNNs are used as controllers for the physical system. Despite their advantages, DNN controllers can produce wrong control decisions, which can lead to safety risks for the system. Once wrong behaviors are detected, the DNN controller should be fixed. DNN repair is a technique that allows to perform this fine-grained improvement. However, state-of-the-art DNN repair techniques require ground-truth labels to guide the repair. For AI-enabled CPSs, these are not available, as it is not possible to assess whether a specific control decision is correct. Nevertheless, it is possible to assess whether the DNN controller leads to wrong behaviors of the controlled system by considering system-level requirements. In this paper, following this observation, we propose a novel DNN repair approach that is guided by system-level specifications. The approach takes in input a system-level specification, some tests violating the specification, and some faulty DNN weights. The approach searches for alternative weight values with the goal of fixing the behavior on the failing tests without breaking the passing tests. We also propose a heuristic that allows us to accelerate the search by avoiding the execution of some tests. Experiments on real-world AI-enabled CPSs show that the approach effectively repairs their controllers.

Delivery systems operated by autonomous robots use schedulers to allocate robots to the different orders. Such schedulers are often optimisation-based algorithms that aim to maximise the number of delivered goods. The oracle problem affects the testing of these schedulers, as it is not always possible to assess whether the schedule produced for a given scenario is the optimal one. In this work, we propose a framework, based on a novel use of metamorphic testing, to assess the optimality of the scheduling algorithm developed by Panasonic for the management of a fleet of autonomous delivery robots in the Fujisawa Sustainable Smart Town, Japan. In the framework, a metamorphic relation (MR) transforms a source test case in a followup test case in a predefined way, and compares the results of the execution of the two tests in a simulated environment: if the comparison violates the expected relation, we can claim that one of the two schedules produced by the scheduler is suboptimal. We propose 19 MRs that target different aspects of the delivery system. Experiments over more than 900,000 test cases show that the different MRs have different abilities in exposing suboptimal behaviour and that most of the MRs do not subsume each other. Moreover, they also show that MR violations can provide useful insights into the scheduler's behaviour to Panasonic's engineers.

The most promising applications of quantum computing are centered around solving search and optimization tasks, particularly in fields such as physics simulations, quantum chemistry, and finance. However, the current quantum software testing methods face practical limitations when applied in industrial contexts: (i) they do not apply to quantum programs most relevant to the industry, (ii) they require a full program specification, which is usually not available for these programs, and (iii) they are incompatible with error mitigation methods currently adopted by main industry actors like IBM. To address these challenges, we present QOPS, a novel quantum software testing approach. QOPS introduces a new definition of test cases based on Pauli strings to improve compatibility with different quantum programs. QOPS also introduces a new test oracle that can be directly integrated with industrial APIs such as IBM's Estimator API and can utilize error mitigation methods for testing on real noisy quantum computers. We also leverage the commuting property of Pauli strings to relax the requirement of having complete program specifications, making QOPS practical for testing complex quantum programs in industrial settings. We empirically evaluate QOPS on 194,982 real quantum programs, demonstrating effective performance in test assessment compared to the state-of-the-art with a perfect F1-score, precision, and recall. Furthermore, we validate the industrial applicability of QOPS by assessing its performance on IBM's three real quantum computers, incorporating both industrial and open-source error mitigation methods.

Autonomous robots are emerging as a solution to various challenges of last mile goods delivery, like reducing traffic congestion, pollution, and costs. The configuration of an autonomous delivery robots system requires balancing aspects like delivery rate, cost of robots' operation, and required monitoring efforts. Our industry partner Panasonic is employing a search-based approach to find the configurations of the system that optimise these three aspects for a given set of customers' orders. The approach uses a simulator to assess the different configurations in the fitness functions' computation. Due to the high cost of the simulation, the whole search-based approach is computationally expensive. A classic approach to speed up such approaches is to use surrogate models trained on example simulation data that allow to approximate the results of a simulated configuration with negligible computational cost. A risk when using such approaches is to underestimate the cost of building the surrogate model itself, that can exceed the computational gain obtained during the search, thus making the adoption of surrogate models detrimental. In this work, we propose an approach in which the surrogate model is not trained before the search; instead, the approach alternates between training the model on subsets of data of increasing size, and searching using these cheaper models until the search stagnates. Experiments over 144,000 settings of the search show that the proposed approach can significantly reduce the cost of searching for configurations, while having an acceptable impact on the Quality of the configurations it finds.

Abstract Modern automotive systems with adaptive control features require rigorous analysis to guarantee correct operation. We report our experience in modeling the automotive case study from the ABZ2020 conference using the ASMETA toolset, based on the Abstract State Machine formal method. We adopted a seamless system engineering method: from an incremental formal specification of high-level requirements to increasingly refined ASMETA models, to the C++ code generation from the model. Along this process, different validation and verification activities were performed. We explored modeling styles and idioms to face the modeling complexity and ensure that the ASMETA models can best capture and reflect specific behavioral patterns. Through this realistic automotive case study, we evaluated the applicability and usability of our formal modeling approach.

The Multi-Agent Path Finding (MAPF) problem, i.e., the scheduling of multiple agents to reach their destinations, has been widely investigated. Testing MAPF systems is challenging, due to the complexity and variety of scenarios and the agents’ distribution and interaction. Moreover, MAPF testing suffers from the oracle problem, i.e., it is not always clear whether a test shows a failure or not. Indeed, only considering whether the agents reach their destinations without collision is not sufficient. Other properties related to the ‘quality’ of the generated paths should be assessed, e.g., an agent should not follow an unnecessarily long path. To tackle this issue, this article proposes MET-MAPF, a Metamorphic Testing approach for MAPF systems. We identified 10 Metamorphic Relations (MRs) that a MAPF system should guarantee, designed over the environment in which agents operate, the behaviour of the single agents and the interactions among agents. Starting from the different MRs, MET-MAPF automatically generates test cases addressing them, so possibly exposing different types of failures. Experimental results show that MET-MAPF can indeed find MR violations not exposed by approaches that only consider the completion of the mission as test oracle. Moreover, experiments show that different MRs expose different types of violations.

Quantum Computing (QC) promises computational speedup over classic computing. However, noise exists in near-term quantum computers. Quantum software testing (for gaining confidence in quantum software's correctness) is inevitably impacted by noise, i.e., it is impossible to know if a test case failed due to noise or real faults. Existing testing techniques test quantum programs without considering noise, i.e., by executing tests on ideal quantum computer simulators. Consequently, they are not directly applicable to test quantum software on real quantum computers or noisy simulators. Thus, we propose a noise-aware approach (named$\mathit{QOIN}$) to alleviate the noise effect on test results of quantum programs.$\mathit{QOIN}$employs machine learning techniques (e.g., transfer learning) to learn the noise effect of a quantum computer and filter it from a program's outputs. Such filtered outputs are then used as the input to perform test case assessments (determining the passing or failing of a test case execution against a test oracle). We evaluated$\mathit{QOIN}$on IBM's 23 noise models, Google's two available noise models, and Rigetti's Quantum Virtual Machine, with six real-world and 800 artificial programs. We also generated faulty versions of these programs to check if a failing test case execution can be determined under noise. Results show that$\mathit{QOIN}$can reduce the noise effect by more than$80\%$on most noise models. We used an existing test oracle to evaluate$\mathit{QOIN}$'s effectiveness in quantum software testing. The results showed that$\mathit{QOIN}$attained scores of$99\%$,$75\%$, and$86\%$for precision, recall, and F1-score, respectively, for the test oracle across six real-world programs. For artificial programs,$\mathit{QOIN}$achieved scores of$93\%$,$79\%$, and$86\%$for precision, recall, and F1-score respectively. This highlights$\mathit{QOIN}$'s effectiveness in learning noise patterns for noise-aware quantum software testing.

Test case optimization (TCO) reduces the software testing cost while preserving its effectiveness. However, to solve TCO problems for large-scale and complex software systems, substantial computational resources are required. Quantum approximate optimization algorithms (QAOAs) are promising combinatorial optimization algorithms that rely on quantum computational resources, with the potential to offer increased efficiency compared to classical approaches. Several proof-of-concept applications of QAOAs for solving combinatorial problems, such as portfolio optimization, energy optimization in power systems, and job scheduling, have been proposed. Given the lack of investigation into QAOA's application for TCO problems, and motivated by the computational challenges of TCO problems and the potential of QAOAs, we present IGDec-QAOA to formulate a TCO problem as a QAOA problem and solve it on both ideal and noisy quantum computer simulators, as well as on a real quantum computer. To solve bigger TCO problems that require many qubits, which are unavailable these days, we integrate a problem decomposition strategy with the QAOA. We performed an empirical evaluation with five TCO problems and four publicly available industrial datasets from ABB, Google, and Orona to compare various configurations of IGDec-QAOA, assess its decomposition strategy of handling large datasets, and compare its performance with classical algorithms (i.e., Genetic Algorithm (GA) and Random Search). Based on the evaluation results achieved on an ideal simulator, we recommend the best configuration of our approach for TCO problems. Also, we demonstrate that our approach can reach the same effectiveness as GA and outperform GA in two out of five test case optimization problems we conducted. In addition, we observe that, on the noisy simulator, IGDec-QAOA achieved similar performance to that from the ideal simulator. Finally, we also demonstrate the feasibility of IGDec-QAOA on a real quantum computer in the presence of noise.

Finding optimal configurations for complex systems, such as a fleets of autonomous delivery robots, is a complex task that benefits from automation. Automated search-based approaches have been proposed to automatically find such configurations. Although the configurations found by these methods perform well on average, they may be non-stable, i.e., their performance could vary greatly across scenarios. When deploying a system with a given configuration, it is important to know that it will perform adequately for the range of possible scenarios, i.e., to reduce how much the system's performance varies between scenarios. To this end, we attempt to make the search-based approaches aware of the configurations' stability. We explore two ways of doing this: by integrating it into the fitness functions describing the target performance metrics, and by adding it as a separate set of additional objectives. We applied the two approaches to find optimal configurations of a fleet of robots for automatic delivery service. Results show that integrating the stability concern into the fitness functions is better than treating it separately.

Abstract Online monitoring is an effective validation approach for hybrid systems, that, at runtime, checks whether the (partial) signals of a system satisfy a specification in, e.g., Signal Temporal Logic (STL) . The classic STL monitoring is performed by computing a robustness interval that specifies, at each instant, how far the monitored signals are from violating and satisfying the specification. However, since a robustness interval monotonically shrinks during monitoring, classic online monitors may fail in reporting new violations or in precisely describing the system evolution at the current instant. In this paper, we tackle these issues by considering the causation of violation or satisfaction, instead of directly using the robustness. We first introduce a Boolean causation monitor that decides whether each instant is relevant to the violation or satisfaction of the specification. We then extend this monitor to a quantitative causation monitor that tells how far an instant is from being relevant to the violation or satisfaction. We further show that classic monitors can be derived from our proposed ones. Experimental results show that the two proposed monitors are able to provide more detailed information about system evolution, without requiring a significantly higher monitoring cost.

Autonomous robots can solve different issues of delivery services, by guaranteeing less traffic congestion, less pollution, and lower operational costs. Designing such type of delivery system based on autonomous robots requires the collaboration of different stakeholders, having different concerns: the store utilising the delivery service that is interested in costs and customer satisfaction, the municipality where the service is operated that is interested in the safety of the service, and the robotic company providing the service that is interested in all previous concerns. Our industrial partner from the robotic domain is designing this type of service in a smart town, and using a simulator for assessing different configurations providing different levels of performance. Since manually designing the configurations is time consuming for engineers, in this paper, we propose a search-based approach (All) that is able to explore the space of service configurations and find the optimal ones that show the tradeoff existing among the different concerns, so that stakeholders can make an informed decision. Since assessing one configuration requires to simulate the service multiple times over different types of customer requests, the approach suffers from scalability issues. Therefore, we propose two improvements of the approach that reduce the number of required simulations (IncrSim), and the duration of the simulation (IncrTime). Ex-periments on different settings show that IncrSim and IncrTime can find results as good as those of All in less time, and better than versions of All executed for the same budget.

The use of autonomous robots for delivery of goods to customers is an exciting new way to provide a reliable and sustainable service. However, in the real world, autonomous robots still require human supervision for safety reasons. We tackle the real-world problem of optimizing autonomous robot timings to maximize deliveries, while ensuring that there are never too many robots running simultaneously so that they can be monitored safely. We assess the use of a recent hybrid machine-learning-optimization approach COIL (constrained optimization in learned latent space) and compare it with a baseline genetic algorithm for the purposes of exploring variations of this problem. We also investigate new methods for improving the speed and efficiency of COIL. We show that only COIL can find valid solutions where appropriate numbers of robots run simultaneously for all problem variations tested. We also show that when COIL has learned its latent representation, it can optimize 10% faster than the GA, making it a good choice for daily re-optimization of robots where delivery requests for each day are allocated to robots while maintaining safe numbers of robots running at once.

Deep Neural Networks (DNNs) are finding a place at the heart of more and more critical systems, and it is necessary to ensure they perform in as correct a way as possible. Search-based repair methods, that search for new values for target neuron weights in the network to better process fault-inducing inputs, have shown promising results. These methods rely on fault localisation to determine what weights the search should target. However, as the search progresses and the network evolves, the weights responsible for the faults in the system will change, and the search will lose in effectiveness. In this work, we propose an adaptive search method for DNN repair that adaptively updates the target weights during the search by performing fault localisation on the current state of the model. We propose and implement two methods to decide when to update the target weights, based on the progress of the search's fitness value or on the evolution of fault localisation results. We apply our technique to two image classification DNN architectures against a dataset of autonomous driving images, and compare it with a state-of-the art search-based DNN repair approach.

Autonomous robots have recently been employed for goods delivery, with the goal of reducing traffic congestion, pollution, and operational costs. The design of such a delivery service requires to select the number of robots, their operating hours, and speed. Requirements from different stakeholders must be considered: customer satisfaction, cost, and safety. To assist with said design, our industry partner Panasonic is employing a search-based approach that tries to find service configurations that optimise the three requirements, on average, across different possible sets of customer requests. The obtained Pareto fronts of solutions show the trade-off existing among the different requirements. Such Pareto fronts, albeit very useful, do not always facilitate an informed decision for the stakeholders, for they provide too many solutions (some of them very similar to each other). To tackle this issue, in this paper we propose two approaches to prune and simplify Pareto fronts. Our approaches consider the standard deviation of objective values across the different sets of customer requests; the intuition is that, if two solutions (expressed in terms of average objective values) overlap based on their standard deviations, they can be considered similar. Based on this intuition, the two pruning approaches group similar solutions and select only one representative for each partition. We assessed these pruning methods on the Pareto fronts obtained with the search-based approach employed by Panasonic. We found that they can significantly reduce the size of the Pareto fronts while retaining a reasonable amount of their unpruned quality (measured in terms of Hypervolume).

Deep Neural Networks (DNNs) are applied in several safety-critical domains and their trustworthiness is of paramount importance. For example, DNNs used in autonomous driving as classifiers should not misclassify detected objects; however, since obtaining perfect accuracy is not possible, special attention should be given to the most critical cases, e.g., pedestrians. This has been confirmed by the consortium of our partners from the automotive domain that provided us with specific risk levels for different misclassifications. A recent approach to improve DNN performance is to localise DNN weights responsible for the misclassifications and then adjust (repair) them to improve the misclassifications. However, they under-perform when they need to consider multiple misclassifications, and they do not consider the risk levels of the different misclassifications. To tackle this, we propose DISTRREP, a distributed repair approach that first finds the best fixes for each critical misclassification, and then integrates them in a single repaired DNN model, by considering the risk levels. We assess DISTRREP over three DNN models and a dataset of autonomous driving images, by considering requirements specified by our industrial partners. Experiments show that DISTRREP is more effective than baseline approaches based on retraining, and other risk-unaware repair approaches.

Collision avoidance systems are fundamental for autonomous driving and need to be tested thoroughly to check whether they safely handle critical scenarios. Testing collision avoidance systems is generally done by means of scenario-based testing using simulators and comes with the main challenge of generating situations that are realistic but avoidable. In other words, driving scenarios must stress the collision avoidance functionalities while being representative. Existing crash databases and accident reports describe observed accidents and enable to (re)create realistic collisions in simulations; however, as those data sources focus on the impact, their data do not generally lead to avoidable collision scenarios. To address this issue, we propose STRETCH, which generates realistic, critical, and avoidable collision scenarios by extending focused collision descriptions using a multi-objective optimization algorithm. Thanks to STRETCH, developers and testers can automatically generate challenging test cases based on realistic crash scenarios.

With the increased developments in quantum computing, the availability of systematic and automatic testing approaches for quantum programs is becoming increasingly essential. To this end, we present the quantum software testing tool QuCAT for combinatorial testing of quantum programs. QuCAT provides two functionalities of use. With the first functionality, the tool generates a test suite of a given strength (e.g., pairwise). With the second functionality, it generates test suites with increasing strength until a failure is triggered or a maximum strength is reached. QuCAT uses two test oracles to check the correctness of test outputs. We assess the cost and effectiveness of QuCAT with 3 faulty versions of 5 quantum programs. Results show that combinatorial test suites with a low strength can find faults with limited cost, while a higher strength performs better to trigger some difficult faults with relatively higher cost.

The recent fast development of quantum computers breaks several computation limitations that are difficult for conventional computers. Up to the present, although many approaches and tools have been proposed to test quantum programs, the fundamental features of quantum programs, i.e., magnitude, phase, and entanglement, have been largely overlooked, leading to limited fault detection capability and reduced testing effectiveness. To address this problem, we propose an automated testing framework named QURATEST, equipped with three test case generators (including two newly proposed techniques, UCNOT and IQFT in this paper, as well as one based on Random techniques) to test quantum programs. Overall, the proposed generators enable the generation of diverse test inputs by considering the quantum features of quantum programs. In the experiments, we perform an in-depth evaluation of QURATEST from three aspects: generated test case diversity, output coverage of the program under test, and fault detection capability. The results demonstrate the potential of our newly proposed techniques in that IQFT can generate the most diverse test cases regarding magnitude, phase, and entanglement, with 66% cell coverage. Comparatively, the Random approach only has 10% cell coverage. Regarding the evaluations of the output coverage, IQFT can achieve the highest output coverage in 70.2% (33 out of 47) of all quantum programs. In terms of fault detection, UCNOT outperforms the other two techniques. Specifically, the test cases generated by UCNOT have the best mutation score in 88.4% (23 out of 26) quantum programs.

Verification of hybrid systems is very challenging, if not impossible, due to their continuous dynamics that leads to infinite state space. As a countermeasure, falsification is usually applied to show that a specification does not hold, by searching for a falsifying input as a counterexample that refutes the specification. A falsification algorithm exploits the quantitative robust semantics of temporal specifications, which provides a numerical robustness that tells how robustly a specification holds or not, and uses it as a guide to explore the input space towards the direction of robustness descent—once negative robustness is observed, it indicates that a falsifying input is found. However, if a falsification algorithm does not return any falsifying input, a user is not sure whether the specification does indeed hold, or there exist counterexamples that the algorithm did not manage to reach. In this case, a measurement on how likely there indeed exists no counterexample in the input space is necessary for better understanding the safety of the system and deciding whether more budget should be allocated for the falsification. To this end, we propose a confidence measure that assesses the likelihood that the system is not falsifiable, i.e., how confident a user should be that a specification holds, given the fact that an algorithm has sampled a set of inputs but did not find any falsifying one. The confidence measure is defined in terms of a coverage criterion of the input space that assesses to which extent the whole input space is explored and a local area is exploited where low robustness is observed. Experiments on commonly-used falsification benchmarks show that our proposed confidence measure is reasonable and can distinguish different specifications.

Autonomous Driving Systems (ADSs) are complex systems that must consider different aspects such as safety, compliance to traffic regulations, comfort, etc. The relative importance of these aspects is usually balanced in a weighted cost function. However, there is generally no optimal set of weights, and different driving situations may require different weights values to guarantee a safe drive. Recent testing approaches can generate diverse driving scenarios in which different ADS configurations lead to various degrees of hazard. These tests need to be properly analyzed to improve the ADS's safety. In this paper, we propose an analysis approach that is able to assess the relation between the ADS configurations and the level of hazard that is obtained in some particular traffic situations. The approach uses fuzzification to partition ADS weights in different categories, and a spectrum-based analysis to identify which weights categories are related to hazard and safety. The occurrence of a hazard could be due to a single weight or to combinations of two or more weights. For scalability, the approach performs an incremental analysis, in which first single weights are considered, and then weight combinations of higher order. The approach has been applied to an industrial path planner.

Autonomous Driving Systems (ADSs) are promising, but must show they are secure and trustworthy before adoption. Simulation-based testing is a widely adopted approach, where the ADS is run in a simulated environment over specific scenarios. Coverage criteria specify what needs to be covered to consider the ADS sufficiently tested. However, existing criteria do not guarantee to exercise the different decisions that the ADS can make, which is essential to assess its correctness. ADSs usually compute their decisions using parameterised rule-based systems and cost functions, such as cost components or decision thresholds. In this article, we argue that the parameters characterise the decision process, as their values affect the ADS’s final decisions. Therefore, we propose parameter coverage, a criterion requiring to cover the ADS’s parameters. A scenario covers a parameter if changing its value leads to different simulation results, meaning it is relevant for the driving decisions made in the scenario. Since ADS simulators are slightly uncertain, we employ statistical methods to assess multiple simulation runs for execution difference and coverage. Experiments using the Autonomoose ADS show that the criterion discriminates between different scenarios and that the cost of computing coverage can be managed with suitable heuristics.

Modern Cyber-Physical Systems (CPSs) that need to perform complex control tasks (e.g., autonomous driving) are increasingly using AI-enabled controllers, mainly based on deep neural networks (DNNs). The quality assurance of such types of systems is of vital importance. However, their verification can be extremely challenging, due to their complexity and uninterpretable decision logic. Falsification is an established approach for CPS quality assurance, which, instead of attempting to prove the system correctness, aims at finding a time-variant input signal violating a formal specification describing the desired behavior; it often employs a search-based testing approach that tries to minimize therobustnessof the specification, given by its quantitative semantics. However, guidance provided by robustness is mostly black-box and only related to the system output, but does not allow to understand whether the temporal internal behavior determined by multiple consecutive executions of the neural network controller has been explored sufficiently. To bridge this gap, in this paper, we make an early attempt at exploring the temporal behavior determined by the repeated executions of the neural network controllers in hybrid control systems and first propose eight time-aware coverage criteria specifically designed for neural network controllers in the context of CPS, which consider different features by design: the simple temporal activation of a neuron, the continuous activation of a neuron for a given duration, and the differential neuron activation behavior over time. Second, we introduce a falsification framework, named$\mathtt {FalsifAI}$, that exploits the coverage information for better falsification guidance. Namely, inputs of the controller that increase the coverage (so improving theexplorationof the DNN behaviors), are prioritized in theexploitationphase of robustness minimization. Our large-scale evaluation over a total of 3 typical CPS tasks, 6 system specifications, 18 DNN models and more than 12,000 experiment runs, demonstrates 1) the advantage of our proposed technique in outperforming two state-of-the-art falsification approaches, and 2) the usefulness of our proposed time-aware coverage criteria for effective falsification guidance.

Mutation testing is often used for designing new tests, and involves changing a program in minor ways, which results in mutated versions of the program, i.e., mutants. An effective test suite should find faults (or kill mutants) with a minimum number of test cases, to save resources required for executing test cases. In this paper, in the context of mutation testing for quantum programs, we present a multi-objective and search-based approach (MutTG) to generate the minimum number of test cases killing as many mutants as possible. MutTG tries to estimate the likelihood that a mutant is equivalent, and uses this as a discount factor in the fitness definition to avoid keeping on trying to kill mutants that cannot be killed. We employed NSGA-II as the multi-objective search algorithm. Then, we compared MutTG with another version of the approach that does not use the discount factor in its fitness definition, and with random search (RS), over a set of open-source quantum programs and their mutants of varying complexity. Results show that the discount factor does indeed help in guiding the test generation, as the approach with the discount factor performs better than the one without it.

Neural networks have been widely applied for performing tasks in critical domains, such as, for example, the medical domain; their robustness is, therefore, important to be guaranteed. In this paper, we propose a robustness definition for neural networks used for regression, by tackling some of the problems of existing robustness definitions. First of all, by following recent works done for classification problems, we propose to define the robustness of networks used for regression w.r.t. alterations of their input data that can happen in reality. Since different alteration levels are not always equally probable, the robustness definition is parameterized with the probability distribution of the alterations. The error done by this type of networks is quantifiable as the difference between the estimated value and the expected value; since not all the errors are equally critical, the robustness definition is also parameterized with a “tolerance” function that specifies how the error is tolerated. The current work has been motivated by the collaboration with the industrial partner that has implemented a medical sensor employing a Multilayer Perceptron for the estimation of the blood oxygen pressure. After having computed the robustness for the case study, we have successfully applied three techniques to improve the network robustness: data augmentation with recombined data, data augmentation with altered data, and incremental learning. All the techniques have proved to contribute to increasing the robustness, though in different ways.

Simulation-based testing is a popular approach for testing autonomous driving systems (ADS), in which different types of scenario are designed to test the ADS under different driving conditions. Given a specific test goal, a generation approach (e.g., search-based testing) is usually employed to find a scenario covering such goal; for example, it can find a scenario in which the autonomous vehicle collides. The generated scenarios may contain some elements that are irrelevant for the achievement of the test goal; if this is the case for a scenario that exposes a failure, for ADS engineers it is difficult to identify the root cause, as the ADS interacts with several traffic participants and it is not clear which of these are essential to trigger the failure. This problem emerged during the collaboration with our industry partner, for which, in the past, we proposed different test generation approaches for their ADS path planner, but these may produce test scenarios that are not minimal. To tackle this problem, in this paper, we propose an approach that, given an ADS test scenario, simplifies it by removing all the traffic participants that are not needed. As output, the approach provides a scenario that still covers the test goal as the initial scenario, but contains the minimum number of traffic participants. The approach consists in iteratively generating simplified scenarios by removing some traffic participants and determining, by observing the test execution, which can be actually removed and which must be kept in the scenario. Three policies are investigated to remove traffic participants whose classification is not know: single policy, binary policy, and adaptive policy. Experiments have been conducted on several scenarios generated for the path planner. Results show that the binary policy is the one that usually can find the minimal scenario with the minimum number of simplification attempts, but, in particular cases, the adaptive policy is better.

The difficulty in exploring the game balance has been increasing, especially in Game-as-a-Service (GaaS) with updates in every few weeks, and due to the complexity in game design and business models. In the limited time available for testing, using automated game agents enables much more test plays than using human test players does, and it has been accelerated by the recent progress of deep reinforcement learning. However, understanding specific behaviours of each agent is hard due to their “black-box” nature. In this paper, we propose a method for explaining the behaviour of game agents using differential comparison between agents. This comparison approach is motivated by our experience with existing explanation techniques that often extracted uninteresting, common aspects of the behaviour. In addition, there are large potentials for the application of the comparison: between agents with different learning algorithms, between human agents and automated agents, and between test agents and users. We applied our technique to a prototype of a commercial GaaS and confirmed our technique can extract specific differences between agents.

Autonomous Driving Systems (ADSs) are complex systems that must satisfy multiple safety requirements. In particular cases, all the requirements cannot be satisfied at the same time, and the control software of the ADS must make trade-offs among their satisfaction. Usually, the trading-offs in the decision-making process are configurable; different configuration options can affect driving behaviors, satisfying or violating requirements at different degrees. Therefore, it is highly important to know whether a configuration can guarantee a safe drive or not, i.e., whether it leads to requirement violations that exceed the allowable range or not. However, there is currently no approach to systematically assess the safety of ADS configurations from the perspective of requirements violations. To bridge this gap, this paper proposes a “Hierarchical Safety Assessment” approach (HSA) that is able to quantitatively analyze the violation severity of safety requirements and distinguish safer ADS configurations based on the requirements violations comparison done in a hierarchical way by following requirements importance. We apply HSA to an industrial ADS under six traffic situations. Evaluation results show that HSA is effective in distinguishing safer configurations and provides useful feedback to ADS engineers to reconfigure the ADS in a better way.

Understanding the performance characteristics of software systems is particular relevant when looking at design alternatives. However, it is a very challenging problem, due to the complexity of interpreting the role and incidence of the different system elements on performance metrics of interest, such as system response time or resources utilisation. This work introduces JSIMutate, a tool that makes use of queueing network performance models and enables the analysis of mutations of a model reflecting possible design changes to support designers in identifying the model elements that contribute to improving or worsening the system's performance.

Performance models have been used in the past to understand the performance characteristics of software systems. However, the identification of performance criticalities is still an open challenge, since there might be several system components contributing to the overall system performance. This work combines two different areas of research to improve the process of interpreting model-based performance analysis results: (i) software performance engineering that provides the ground for the evaluation of the system’s performance; (ii) mutation-based techniques that nicely supports the experimentation of changes in performance models and contribute to a more systematic assessment of performance indices. We propose mutation operators for specific performance models, i.e., queueing networks, that resemble changes commonly made by designers when exploring the properties of a system’s performance. Our approach consists in introducing a mutation-based approach that generates a set of mutated queueing network models. The performance of these mutated networks is compared to that of the original network to better understand the effect of variations in the different components of the system. A set of benchmarks is adopted to show how the technique can be used to get a deeper understanding of the performance characteristics of software systems.

Online monitoring is a popular validation approach in which the temporal behavior of a system is checked to assess whether it satisfies a given specification expressed, e.g., in signal temporal logic (STL). This is done by employing a monitor that, at each time point, states the specification validity: satisfied, violated, or unknown. In some settings, monitoring should continue even after a violation episode is detected, to detect possible future violation episodes. However, for a monitor just relying on STL semantics, this is not possible, as, once the specification is violated by an input signal, any continuation of the signal still violates the specification. To tackle this problem, we here propose an optimal reset technique that, at runtime, detects the end of a violation episode and shifts the evaluation of the monitor to skip such an episode. In this way, the monitoring can continue to detect possible other future violation episodes. We propose a framework that integrates the reset technique with an existing monitoring approach. Experiments on two Simulink models show that the technique can effectively reset the monitor and report all the violation episodes, with a negligible overhead on the monitoring cost.

Abstract Hybrid system falsification is an important quality assurance method for cyber-physical systems with the advantage of scalability and feasibility in practice than exhaustive verification. Falsification, given a desired temporal specification, tries to find an input of violation instead of a proof guarantee. The state-of-the-art falsification approaches often employ stochastic hill-climbing optimization that minimizes the degree of satisfaction of the temporal specification, given by its quantitativerobust semantics. However, it has been shown that the performance of falsification could be severely affected by the so-calledscale problem, related to the different scales of the signals used in the specification (e.g., rpm and speed): in the robustness computation, the contribution of a signal could bemaskedby another one. In this paper, we propose a novel approach to tackle this problem. We first introduce a new robustness definition, calledQB-Robustness, which combines classical Boolean satisfaction and quantitative robustness. We prove that QB-Robustness can be used to judge the satisfaction of the specification and avoid the scale problem in its computation. QB-Robustness is exploited by a falsification approach based on Monte Carlo Tree Search over the structure of the formal specification. First, tree traversal identifies the sub-formulas for which it is needed to compute the quantitative robustness. Then, on the leaves, numerical hill-climbing optimization is performed, aiming to falsify such sub-formulas. Our in-depth evaluation on multiple benchmarks demonstrates that our approach achieves better falsification results than the state-of-the-art falsification approaches guided by the classical quantitative robustness, and it is largely not affected by the scale problem.

Due to the complexity of designing vehicle products and the inherent uncertainties in their operating environments, ensuring the safety of their Advanced Driver Assistance Systems (ADASs) becomes crucial. Especially, very minor changes to a vehicle design, for instance due to production errors or component degradation, might lead to failures of ADASs and, therefore, catastrophic consequences such as collision occurrences. Motivated by this, we propose a multi-objective search-based approach (employing NSGA-II) to find minimum changes to the configuration of a set of configurable parameters of a vehicle design, such that the collision probability is maximized, consequently leading to a reversal change in its safety. We conducted experiments, in a vehicle driving simulator, to evaluate the effectiveness of our approach. Results show that our approach with NSGA-II significantly outperforms the random search. Moreover, based on the detailed analyses of the results, we identify some parameters for which minor changes to their values lead the vehicle into collisions, and demonstrated the importance of studying the configuration of multiple parameters in a single search and the impact of their interactions on causing collisions.

Quantum programs implement quantum algorithms solving complex computational problems. Testing such programs is challenging due to the inherent characteristics of Quantum Computing (QC), such as the probabilistic nature and computations in superposition. However, automated and systematic testing is needed to ensure the correct behavior of quantum programs. To this end, we present an approach called Quito (QUantum InpuT Output coverage) consisting of three coverage criteria defined on the inputs and outputs of a quantum program, together with their test generation strategies. Moreover, we define two types of test oracles, together with a procedure to determine the passing and failing of test suites with statistical analyses. To evaluate the cost-effectiveness of the three coverage criteria, we conducted experiments with five quantum programs. We used mutation analysis to determine the coverage criteria' effectiveness and cost in terms of the number of test cases. Based on the results of mutation analysis, we also identified equivalent mutants for quantum programs.

Classification using Artificial Neural Networks (ANNs) is widely applied in critical domains, such as autonomous driving and in the medical practice; therefore, their validation is extremely important. A common approach consists in assessing the network robustness, i.e., its ability to correctly classify input data that is particularly challenging for classification. We recently proposed a robustness definition that considers input data degraded by alterations that may occur in reality; the approach was originally devised for image classification in the medical domain. In this paper, we extend the definition of robustness to any type of input for which some alterations can be defined. Then, we present ROBY, a tool for ROBustness analYsis of ANNs. The tool accepts different types of data (images, sounds, text, etc.) stored either locally or on Google Drive. The user can use some alterations provided by the tool, or define their own. The robustness computation can be performed either locally or remotely on Google Colab. The tool has been experimented for robustness computation of image and sound classifiers, used in the medical and automotive domains.

A common approach in testing automated and autonomous driving systems (ADS) consists in running the ADS in a simulator where driving and environmental conditions are specified in terms of scenarios. An important aspect in ADS testing is to cover different driving situations in which the autonomous car must perform different types of maneuvers. In this paper, we consider the path planner of our industry partner; the path planner is responsible for deciding the path that must be followed by the autonomous car. A path is characterized by the driving characteristics (as forward acceleration, lateral acceleration, curvature, and so on) that are needed, at each time point, to implement it. For different driving characteristics, a good test suite should contain a scenario for which the path planner chooses a path that requires the application of the selected driving characteristics for a non-negligible period of time: this means that the characteristics are relevant in that path. With such a test suite, engineers can observe the different types of decision taken by the path planner, and so possibly better assess its correctness. In the paper, we introduce the notion of patterns of driving characteristics, to characterize their interaction (i.e., simultaneous or not) and measure their duration. Exploiting this definition, we propose two search-based approaches (for single and pairs of driving characteristics) to find scenarios in which such patterns occur and their duration is maximized. Experimental results show that the approaches are effective in finding scenarios for which the path planner generates paths where the different driving characteristics occur in terms of the specified pattern.

Validating Deep Neural Networks (DNNs) used for classification is of paramount importance; an approach for this consists in (i) executing the DNN over the test dataset, (ii) collecting information about classifications, and (iii) applying fault localization (FL) techniques to identify the neurons responsible for the misclassifications. DNNs can have multiple misclassification types, and so neurons responsible for one type could be different from those responsible for another type. However, depending on the granularity of the analyzed dataset, FL may not reveal these differences: failure types more frequent in the dataset may mask less frequent ones. We here propose a way to perform FL for DNNs that avoids this masking effect by selecting test data in a granular way. We conduct an empirical study, using a spectrum-based FL approach for DNNs, to assess how FL results change by changing the granularity of the analyzed test data. Namely, we perform FL by using test data with two different granularities: following a state-of-the-art approach that considers all misclassifications for a given class together, and the proposed fine-grained approach. Results show that FL should be done for each misclassification, such that practitioners have a more detailed analysis of the DNN faults and can make a more informed decision on what to fix in the DNN.

Decision systems such as Multiple-Criteria Decision Analysis systems formulate a decision process in terms of a mathematical function that takes into consideration different aspects of a problem. Testing such systems is crucial, as they are usually employed in safety-critical systems. A good test suite for these systems should be able to exercise all the possible types of decisions that can be taken by the system. Classic structural coverage criteria do not provide good test suites in this sense, as they can be fulfilled by simple tests that only cover one possible type of decision. Thus, in this paper we discuss the need for tailored coverage criteria for this class of systems, and we propose a criterion based on the perturbation of the decision systems’ parameters. We demonstrate the effectiveness of the criterion, compared to classic structural coverage criteria, on a path planner system for autonomous driving. We also discuss other benefits, such as the criterion helping explain why a decision was made during a test.

Autonomous Driving Systems (ADSs) are complex systems that must satisfy multiple requirements such as safety, compliance to traffic rules, and comfortableness. However, satisfying all these requirements may not always be possible due to emerging environmental conditions. Therefore, the ADSs may have to make trade-offs among multiple requirements during the ongoing operation, resulting in one or more requirements violations. For ADS engineers, it is highly important to know which combinations of requirements violations may occur, as different combinations can expose different types of failures. However, there is currently no testing approach that can generate scenarios to expose different combinations of requirements violations. To address this issue, in this paper, we introduce the notion of requirements violation pattern to characterize a specific combination of requirements violations. Based on this notion, we propose a testing approach named EMOOD that can effectively generate test scenarios to expose as many requirements violation patterns as possible. EMOOD uses a prioritization technique to sort all possible patterns to search for, from the most to the least critical ones. Then, EMOOD iteratively includes an evolutionary many-objective optimization algorithm to find different combinations of requirements violations. In each iteration, the targeted pattern is determined by a dynamic prioritization technique to give preferences to those patterns with higher criticality and higher likelihood to occur. We apply EMOOD to an industrial ADS under two common traffic situations. Evaluation results show that EMOOD outperforms three baseline approaches in generating test scenarios by discovering more requirements violation patterns.

Given that quantum software testing is a new area of research, there is a lack of benchmark programs and bugs repositories to assess the effectiveness of testing techniques. To this end, quantum mutation analysis focuses on systematically generating faulty versions of Quantum Programs (QPs), called mutants, using mutation operators. Such mutants can be used as benchmarks to assess the quality of test cases in a test suite. Thus, we present Muskit - a quantum mutation analysis tool for QPs coded in IBM's Qiskit language. Muskit defines mutation operators on gates of QPs and selection criteria to reduce the number of mutants to generate. Moreover, it allows for the execution of test cases on mutants and generation of results for test analyses. Muskit is provided as command line interface, GUI, and web application. We validated Muskit by using it to generate and execute mutants for four QPs. Muskit code: https://github.com/Simula-COMPLEX/muskitWeb app: https://qiskitmutantcreatorsrl.pythonanywhere.com/YouTube Video: EbPHJOK_AEA Artifact Available: https://doi.org/10.5281/zenodo.5288917

Automation in quantum software testing is essential to support systematic and cost-effective testing. Towards this direction, we present a quantum software testing tool called Quito that can automatically generate test suites covering three coverage criteria defined on inputs and outputs of a quantum program coded in Qiskit, i.e., input coverage, output coverage, and input-output coverage. Quito also implements two types of test oracles based on program specifications, i.e., checking whether a quantum program produced a wrong output or checking a probabilistic test oracle with statistical test. We describe the architecture and methodology of the tool. We also validated the tool with one quantum program and one faulty version of it. Results indicate that Quito can generate test suites and perform test assessments that detect faults, and produce test results with a good time performance.Quito’s code: https://github.com/Simula-COMPLEX/quitoQuito’s video: https://youtu.be/kuI9QaCo8A8Artifact Available: https://doi.org/10.5281/zenodo.5288665

This paper presents the first evaluation of k-nearest neighbours-Averaging (kNN-Avg) on a real-world case study. kNN-Avg is a novel technique that tackles the challenges of noisy multi-objective optimisation (MOO). Existing studies suggest the use of repetition to overcome noise. In contrast, kNN-Avg approximates these repetitions and exploits previous executions, thereby avoiding the cost of re-running. We use kNN-Avg for the scenario generation of a real-world autonomous driving system (ADS) and show that it is better than the noisy baseline. Furthermore, we compare it to the repetition-method and outline indicators as to which approach to choose in which situations.

Validating Autonomous Driving Systems (ADSs) is essential to ensure that the ADS meets the necessary requirements to be widely accepted. Simulation-based testing is one of the main validation approaches, in which the ADS is run in a simulated environment over different scenarios. In this context, search-based testing (SBT) is used to generate scenarios that possibly expose particular failures of the ADS under test. Most SBT approaches search for behaviors of other traffic participants, but usually fix the road map of the scenario in advance. Recently, the SBT community started investigating the search for road structures, which is particularly useful when testing specific components of the ADS, such as the lane-keeping component. However, roads can be represented in multiple ways and the impact of using a particular representation on the effectiveness of SBT is unclear. To fill this gap, this paper investigates the usage of six road representations for SBT of ADSs. As a representative SBT approach, we test the lane-keeping component of an ADS in the BeamNG.tech simulator, aiming to generate roads in which the autonomous vehicle drives off the lane. We study the effectiveness of each road representation in terms of triggered failures and also diversity of the generated roads.

The capability of Quantum Computing (QC) in solving complex problems has been increasingly recognized. However, similar to classical computing, to fully exploit QC's potential, it is important to ensure the correctness of quantum programs. Doing so via software testing is, however, very challenging because of QC's inherent properties: superposition and entanglement. Towards the direction of ensuring the correctness of quantum programs, we propose an approach called QuCAT (QUantum CombinAtorial Testing) for systematic and automated testing of quantum programs by benefiting from combinatorial testing, which has been proven to be cost-effective in testing classical programs. QuCAT supports two combinatorial test suite generation scenarios, i.e., generating combinatorial test suites of a given strength, and incrementally generating and executing combinatorial test suites of increasing strength until a fault is found. The approach employs two types of test oracles to assess test results. We performed an empirical study with 18 faulty versions of quantum programs to evaluate QuCAT with strengths of two, three, and four in the two test generation scenarios. We compare the cost-effectiveness of combinatorial testing of various strengths and random testing (taken as baseline approach). Results show that combinatorial testing always performs better than random testing with the same cost and finds faults more quickly (in terms of required number of test cases). In addition, in most cases, combinatorial testing with a higher strength outperforms the lower strength in terms of effectiveness.

The oracle problem is a key issue in testing Autonomous Driving Systems (ADS): when a collision is found, it is not always clear whether the ADS is responsible for it. Our recent search-based testing approach offers a solution to this problem by defining a collision as avoidable if a differently configured ADS would have avoided it. This approach searches for both collision scenarios and the ADS configurations capable of avoiding them. However, its main problem is that the ADS configurations generated for avoiding some collisions are not suitable for preventing other ones. Therefore, it does not provide any guidance to automotive engineers for improving the safety of the ADS. To this end, we propose a new search-based approach to generate configurations of the ADS that can avoid as many different types of collisions as possible. We present two versions of the approach, which differ in the way of searching for collisions and alternative configurations. The approaches have been experimented on the path planner component of an ADS provided by our industry partner.

Autonomous Driving Systems (ADS) are complex critical systems that need to be thoroughly tested. Still, assessing the strength of tests for such systems is an open and complex problem. A central component of an ADS is the Path Planner, which is in charge of computing the trajectory of the autonomous vehicle. It bases its decisions on several aspects such as safety, traffic regulations, comfort, etc. These aspects can be linked to weights in a weighted cost function that ranks potential trajectories to be followed. Weight coverage has been proposed as a test criterion for tests of this type of path planner. Weight coverage measures how much the different weights (and thus the aspects they are linked to) are involved in the decisions taken by the path planner in a test scenario. All weights should be involved in at least one test. Although weight coverage has shown to be a reasonable criterion, it does not provide a clear way to drive the generation of new scenarios. In this paper, we propose a search-based approach for generating scenarios for achieving weight coverage. We introduce two variants of the approach; the first one tries to generate a scenario covering a given single weight, while the second one tries to generate scenarios covering as many weights as possible at the same time. We experimented with these approaches using the path planner provided by our industry partner, and we show that they are able to generate scenarios that cover all the weights.

Automated and autonomous driving systems (ADS) are a transformational technology in the mobility sector. Current practice for testing ADS uses virtual tests in computer simulations; search-based approaches are used to find particularly dangerous situations, possibly collisions. However, when a collision is found, it is not always easy to automatically assess whether the ADS should have been able to avoid it, without relying on offline analyses by domain experts. In this paper, we propose a definition of avoidable collision that does not rely on any domain knowledge, but only on the fact that it is possible to reconFigure the ADS (in our case, the path planner component provided by our industry partner) in a way that the collision is avoided. Based on this definition, we propose two search-based approaches for finding avoidable collisions. The first one (named sequential approach), based on current industrial practice, first searches for a collision, and then searches for an alternative configuration of the ADS which avoids it. The second one (named combined approach), instead, searches at the same time for the collision and for the alternative configuration which avoids it. Experiments show that the combined approach finds more avoidable collisions, even when the sequential approach doesn't find any; indeed, the sequential approach, in the first search, may find too severe collisions for which there is no alternative configuration that can avoid them.

Typical approaches to test Autonomous Driving Systems (ADS) generate tests in a simulation environment. A common goal in ADS testing is to find scenarios in which the car collides, as these could witness ADS faults. Recent approaches not only find a collision, but they also show whether it could be avoided: they search for a different ADS configuration (i.e., the setting of some parameters) using which the car does not collide. However, such techniques do not explain why the collision occurs and why the alternative configuration is able to avoid it. In this paper, we propose an approach to investigate the relationship between the ADS configurations and the obtained safety during driving. We first use a technique based on fuzzification to partition ADS parameters in different categories, and a spectra- based analysis to identify which categories relate to hazard and safety. Then, we consider collision scenarios by inspecting how the different ADS configurations affect the driving characteristics (e.g., acceleration and curvature) and, so, cause or avoid a collision. We applied the approach to the path planner of our industry partner, by considering three traffic situations. We observed that the path planner, to guarantee safety, should be configured differently in different situations.

The verification of hybrid systems is intrinsically hard, due to the continuous dynamics that leads to infinite search spaces. Therefore, research attempts focused on hybrid system falsification of a black-box model, a technique that aims at finding an input signal violating the desired temporal specification. Main falsification approaches are based on stochastic hill-climbing optimization, that tries to minimize the degree of satisfaction of the temporal specification, given by its robust semantics. However, in the presence of constraints between the inputs, these methods become less effective. In this article, we solve this problem using a search space transformation that first maps points of the unconstrained search space to points of the constrained one, and then defines the fitness of the former ones based on the robustness values of the latter ones. Based on this search space transformation, we propose a falsification approach that performs the search over the unconstrained space, guided by the robustness of the mapped points in the constrained space. We introduce three versions of the proposed approach that differ in the way of selecting the mapped points. Experiments show that the proposed approach outperforms state-of-the-art constrained falsification approaches.

Search-Based Software Engineering (SBSE) researchers who apply multi-objective search algorithms (MOSAs) often assess the quality of solutions produced by MOSAs with one or more quality indicators (QIs). However, SBSE lacks evidence providing insights on commonly used QIs, especially about agreements among them and their relations with SBSE problems and applied MOSAs. Such evidence about QIs agreements is essential to understand relationships among QIs, identify redundant QIs, and consequently devise guidelines for SBSE researchers to select appropriate QIs for their specific contexts. To this end, we conducted an extensive empirical evaluation to provide insights on commonly used QIs in the context of SBSE, by studying agreements among QIs with and without considering differences of SBSE problems and MOSAs. In addition, by defining a systematic process based on three common ways of comparing MOSAs in SBSE, we present additional observations that were automatically produced based on the results of our empirical evaluation. These observations can be used by SBSE researchers to gain a better understanding of the commonly used QIs in SBSE, in particular, regarding their agreements. Finally, based on the results, we also provide a set of guidelines for SBSE researchers to select appropriate QIs for their particular context.

Autonomous cars are subjected to several different kind of inputs (other cars, road structure, etc.) and, therefore, testing the car under all possible conditions is impossible. To tackle this problem, scenario-based testing for automated driving defines categories of different scenarios that should be covered. Although this kind of coverage is a necessary condition, it still does not guarantee that any possible behaviour of the autonomous car is tested. In this paper, we consider the path planner of an autonomous car that decides, at each timestep, the short-term path to follow in the next few seconds; such decision is done by using a weighted cost function that considers different aspects (safety, comfort, etc.). In order to assess whether all the possible decisions that can be taken by the path planner are covered by a given test suite T, we propose a mutation-based approach that mutates the weights of the cost function and then checks if at least one scenario of T kills the mutant. Preliminary experiments on a manually designed test suite show that some weights are easier to cover as they consider aspects that more likely occur in a scenario, and that more complicated scenarios (that generate more complex paths) are those that allow to cover more weights.

Hybrid system falsification is an actively studied topic, as a scalable quality assurance methodology for real-world cyber-physical systems. In falsification, one employs stochastic hill-climbing optimization to quickly find a counterexample input to a black-box system model. Quantitative robust semantics is the technical key that enables use of such optimization. In this paper, we tackle the so-called scale problem regarding Boolean connectives that is widely recognized in the community: quantities of different scales (such as speed [km/h] vs. rpm, or worse, rph) can mask each other’s contribution to robustness. Our solution consists of integration of the multi-armed bandit algorithms in hill climbing-guided falsification frameworks, with a technical novelty of a new reward notion that we call hill-climbing gain. Our experiments show our approach’s robustness under the change of scales, and that it outperforms a state-of-the-art falsification tool.

Safety assurance for automotive products is crucial and challenging. It becomes even more difficult when the variability in automotive products is considered. Recently, the notion of automotive multi-product lines (multi-PL) is proposed as a unified framework to accommodate different sources of variability in automotive products. In the context of automotive multi-PL, we propose a stability analysis for safety, motivated by our industrial collaboration, where we observed that under certain operation scenarios, safety varies drastically with small fluctuations in production parameters, environmental conditions, or driving inputs. To characterize instability, we formulate a multi-objective optimization problem, and solve it with a search-based approach. The proposed technique is applied to an industrial automotive multi-PL, and experimental results show its effectiveness to spot instability. Moreover, based on information gathered during the search, we provide some insights on both testing and quality engineering of automotive products.

Safety assessment of automotive systems is highly demanded, as failure of such systems can lead to dramatic consequences. Usually, these systems are affected by some variability as they contain some production parameters (e.g., the car power, or the braking force) that may drastically affect the behaviour of the system, and so the safety guarantees. Moreover, these systems operate in diverse environmental conditions (e.g., dry or slippery road) that may also affect the system behaviour (we name them as environmental parameters). Classical verification/validation techniques perform safety assessment by considering one particular instance of the system in one particular environmental setting. However, they do not assess the influence of system variability on the final safety. In this paper, we propose a framework for assessing the relation of production and environmental parameters with the overall safety. We first propose an approach based on simulation that assigns hazard degrees to partitions of each parameter domain (defined in terms of fuzzy sets). However, the safety could be affected by interactions of different parameters. Therefore, we also propose a clustering approach that aims at identifying patterns of parameter values providing similar hazard degrees. The approaches have been experimented on an industrial case study related to an automotive collision avoidance system implemented in Simulink. Critical parameters and parameter patterns related to potential collisions were identified and explained.

Summary Regular expressions are used to characterize sets of strings (ie, languages) using a pattern‐based syntax. They are applied in different contexts as, for example, data validation in Web forms. However, writing a regular expression that exactly captures the desired set of strings could be particularly difficult, and techniques are sought to validate regular expressions or test their use in applications. A common means to regular expression validation and testing is the generation of a set of labelled strings (ie, strings together with their evaluation). We here propose a fault‐based approach for generating strings usable as tests for regular expressions. We define some fault classes representing mistakes that could be made when writing a regular expression, and we introduce the notion of distinguishing string, ie, a string that is able to expose a fault. Given a regular expression, our approach generates a test suite composed of distinguishing strings that are able to detect possible faults in the regular expression. We present different versions of the approach, which provide different results in terms of test suite size and generation time. Experiments show that the proposed approach can generate compact test suites and that, using suitable optimizations, the generation time is reasonable. Exploiting the proposed fault classes, we use the notion of mutation score to assess the ability of a generic set of strings in exposing possible faults contained in the regular expression under test. A comparison with other test generation tools in terms of mutation score, size, and generation time shows the advantages and limits of our approach.

Model-based test generation by model checking is a well-known testing technique that, however, suffers from the state explosion problem of model checking and it is, therefore, not always applicable. In this paper, we address this issue by decomposing a system model into suitable subsystem models separately analyzable. Our technique consists in decomposing that portion of a system model that is of interest for a given testing requirement, into a tree of subsystems by exploiting information on model variable dependency. The technique generates tests for the whole system model by merging tests built from those subsystems. We measure and report effectiveness and efficiency of the proposed decomposition-based test generation approach, both in terms of coverage and time.

Few real-world hybrid systems are amenable to formal verification, due to their complexity and black box components. Optimization-based falsification-a methodology of search-based testing that employs stochastic optimization-is thus attracting attention as an alternative quality assurance method. Inspired by the recent work that advocates coverage and exploration in falsification, we introduce a two-layered optimization framework that uses Monte Carlo tree search (MCTS), a popular machine learning technique with solid mathematical and empirical foundations (e.g., in computer Go). MCTS is used in the upper layer of our framework; it guides the lower layer of local hill-climbing optimization, thus balancing exploration and exploitation in a disciplined manner. We demonstrate the proposed framework through experiments with benchmarks from the automotive domain.

NuSMV is a well-known tool for system verification that permits to verify both CTL and LTL properties. Although the tool is very powerful, it offers a minimal support for the editing and validation (e.g., by simulation) of models and of requirements specified as temporal properties. In this paper, we propose NuSeen, a framework that assists a designer during the modeling and V&V activities when using NuSMV. In addition to an editor furnished with syntax highlighting, autocompletion, and outline, NuSeen also provides some tools for visualizing the variable dependencies, and graphically visualizing the counterexamples. It helps the designer in validating the model by checking certain qualities like minimality and completeness. Moreover, the framework also provides facilities for model-based testing by means of a test suite generator that is able to generate tests achieving value and decision coverage for NuSMV models.

Feedback control loops that monitor and adapt managed parts of a software system are considered crucial for realizing self-adaptation in software systems. The MAPE-K (Monitor-Analyze-Plan-Execute over a shared Knowledge) autonomic control loop is the most influential reference control model for self-adaptive systems. The design of complex distributed self-adaptive systems having decentralized adaptation control by multiple interacting MAPE components is among the major challenges. In particular, formal methods for designing and assuring the functional correctness of the decentralized adaptation logic are highly demanded. This article presents a framework for formal modeling and analyzing self-adaptive systems. We contribute with a formalism, called self-adaptive Abstract State Machines , that exploits the concept of multiagent Abstract State Machines to specify distributed and decentralized adaptation control in terms of MAPE-K control loops, also possible instances of MAPE patterns. We support validation and verification techniques for discovering unexpected interfering MAPE-K loops, and for assuring correctness of MAPE components interaction when performing adaptation.

Building a feature model for an existing SPL can improve the automatic analysis of the SPL and reduce the effort in maintenance. However, developing a feature model can be error prone, and checking that it correctly identifies each actual product of the SPL may be unfeasible due to the huge number of possible configurations. We apply mutation analysis and propose a method to detect and remove conformance faults by selecting special configurations that distinguish a feature model from its mutants. We propose a technique that, by iterating this process, is able to repair a faulty model. We devise several variations of a simple hill climbing algorithm for automatic fault removal and we compare them by a series of experiments on three different sets of feature models. We find that our technique is able to improve the conformance of around 90% of the models and find the correct model in around 40% of the cases.

Abstract The request of formal methods for the specification and analysis of distributed systems is nowadays increasing, especially when considering the development of Cloud systems and Web applications. This is due to the fact that modeling languages currently used in these areas have informal definitions and ambiguous semantics, and therefore their use may be unreliable. Thanks to their mathematical foundation, formal methods can guarantee rigorous system design, leading to precise models where requirements can be validated and properties can be assured, already at the early stages of the system development. In this paper, we present a rigorous engineering process for distributed systems, based on the Abstract State Machines (ASM) formal method. We rely on the foundational notions of ASM ground model and model refinement to obtain a precise model for a client-server application for Cloud systems. This application has been proposed to tackle the problem of making Cloud services usable to different end-devices by adapting on-the-fly the content coming from the Cloud to the different devices contexts. The ASM-based modeling process is supported by a number of validation and verification activities that have been exploited on the component under development to guarantee consistency, correctness, and reliability properties.

We present a novel fault-based approach for testing feature models (FMs). We identify several fault classes that represent possible mistakes one can make during feature modeling. We introduce the concept of distinguishing configuration, i.e., a configuration that is able to detect a given fault. Starting from this definition, we devise a technique, based on the use of a logic solver, able either to find distinguishing configurations to be used as tests or to prove that a mutation produces an equivalent feature model. Compact test suites can be produced by exploiting an SMT solver. The experiments show that our methodology is viable and produces reasonable sized test suites in a short time. W.r.t. the approaches that use only the products, our approach has a better fault detection capability and requires fewer tests.

Medical device software malfunctioning can lead to injuries or death for humans and, therefore, its development should adhere to certification standards. However, these standards establish general guidelines on the use of common software engineering activities without any indication regarding methods and techniques to assure safety and reliability. This paper presents a formal development process, based on the Abstract State Machine method, that integrates most of the activities required by the standards. The process permits to obtain, through a sequence of refinements, more detailed models that can be formally validated and verified. Offline and online testing techniques permit to check the conformance of the implementation w.r.t. the specification. The process is applied to the validation of the SAM medical software, that is used to measure the patients' stereoacuity in the diagnosis of amblyopia.

One of the well-known techniques for model-based test generation exploits the capability of model checkers to return counterexamples upon property violations. However, this approach is not always optimal in practice due to the required time and memory, or even not feasible due to the state explosion problem of model checking. A way to mitigate these limitations consists in decomposing a system model into suitable subsystem models separately analyzable. In this paper, we show a technique to decompose a system model into subsystems by exploiting the model variables dependency, and then we propose a test generation approach which builds tests for the single subsystems and combines them later in order to obtain tests for the system as a whole. Such approach mitigates the exponential increase of the test generation time and memory consumption, and, compared with the same model-based test generation technique applied to the whole system, shows to be more efficient. We prove that, although not complete, the approach is sound.

In the context of automatic test generation, the use of propositional satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers is becoming an attractive alternative to traditional algorithmic test generation methods, especially when testing Boolean expressions. The main advantages are the capability to deal with constraints over the inputs, the generation of compact test suites and the support for fault-detecting test generation methods. However, these solvers normally require more time and a greater amount of memory than classical test generation algorithms, making their applicability not always feasible in practice. In this paper, we propose several ways to optimize the SAT/SMT-based process of test generation for Boolean expressions and we compare several solving tools and propositional transformation rules. These optimizations promise to make SAT/SMT-based techniques as efficient as standard methods for testing purposes, especially when dealing with Boolean expressions, as proved by our experiments.

Summary Among validation techniques,model reviewis a static analysis approach that can be performed at the early stages of software development, at the specification level, and aims at determining if a model owns certain quality attributes (like completeness, consistency and minimality). However, the model review capability to detect behavioural faults has never been measured. In this paper, a methodology and a supporting tool for evaluating the fault detection capability of a NuSMV model advisor are presented, which performs an automatic static model review of NuSMV models. The approach is based on the use ofmutationin a similar way as in mutation testing: several mutation operators for NuSMV models are defined, and the model advisor is used to detect behavioural faults by statically analysing mutated specifications. In this way, it is possible to measure the model advisor ability to discover faults. To improve the quality of the analysis, the equivalence between a NuSMV model and any of its mutants must be checked. To perform this task, this paper proposes a technique based on the concept of equivalent Kripke structures, as NuSMV models are Kripke structures. A number of experiments assess the fault‐detecting capability, precision and accuracy of the proposed approach. Analysis of variance is used to check if the results are statistically significant. Some relationships among mutation operators and model quality attributes are also established. Copyright © 2014 John Wiley & Sons, Ltd.

Recent advances in propositional satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers are increasingly rendering SAT and SMT-based automatic test generation an attractive alternative to traditional algorithmic test generation methods. The use of SAT/SMT solvers is particularly appealing when testing Boolean expressions: These tools are able to deal with constraints over the models, generate compact test suites, and they support fault-based test generation methods. However, these solvers normally require more time and greater amount of memory than classical test generation algorithms, limiting their applicability. In this paper we propose several ways to optimize the process of test generation and we compare several SAT/SMT solvers and propositional transformation rules. These optimizations promise to make SAT/SMT-based techniques as efficient as standard methods for testing purposes, especially when dealing with Boolean expressions, as proved by our experiments.

Abstract This paper presents a model‐driven software process suitable to develop a set of integrated tools around a formal method. This process exploits concepts and technologies of the Model‐driven Engineering (MDE) approach, such as metamodelling and automatic generation of software artifacts from models. We describe the requirements to fulfill and the development steps of this model‐driven process. As a proof‐of‐concept, we apply it to the Finite State Machines and we report our experience in engineering a metamodel‐based language and a toolset for the Abstract State Machine formal method. Copyright © 2011 John Wiley & Sons, Ltd.