ABSTRACT Machine Learning (ML) models, such as deep neural networks, are widely applied in autonomous systems to perform complex perception tasks. New dependability challenges arise when ML predictions are used in safety‐critical applications, like autonomous cars and surgical robots. Thus, the use of fault tolerance mechanisms, such as safety monitors, is essential to ensure the safe behavior of the system despite the occurrence of faults. This paper presents an extensive literature review on safety monitoring of perception functions using ML in a safety‐critical context. In this review, we structure the existing literature to highlight key factors to consider when designing such monitors: threat identification, requirements elicitation, detection of failure, reaction, and evaluation. We also highlight the ongoing challenges associated with safety monitoring and suggest directions for future research.

Critical software systems require stringent testing to identify possible failure cases, which can be difficult to find using manual testing. In this study, we report our industrial experience in testing a realistic R&D flight control system using a heuristic based testing method. Our approach utilizes evolutionary strategies augmented with intrinsic motivation to yield a diverse range of test cases, each revealing different potential failure scenarios within the system. This diversity allows for a more comprehensive identification and understanding of the system’s vulnerabilities. We analyze the test cases found by evolution to identify the system’s weaknesses. The results of our study show that our approach can be used to improve the reliability and robustness of avionics systems by providing high-quality test cases in an efficient and cost-effective manner.

In this work, we propose SENA, a run-time monitor focused on detecting unreliable predictions from machine learning (ML) classifiers. The main idea is that instead of trying to detect when an image is out-of-distribution (OOD), which will not always result in a wrong output, we focus on detecting if the prediction from the ML model is not reliable, which will most of the time result in a wrong output, independently of whether it is in-distribution (ID) or OOD. The verification is done by checking the similarity between the neural activations of an incoming input and a set of representative neural activations recorded during training. SENA uses information from true-positive and false-negative examples collected during training to verify if a prediction is reliable or not. Our approach achieves results comparable to state-of-the-art solutions without requiring any prior OOD information and without hyperparameter tuning. Besides, the code is publicly available for easy reproducibility at https://github.com/raulsenaferreira/SENA.

Pairwise testing (PT) exercises the interactions of pairs of input parameters. The approach is classically defined for a flat set of parameters, the number of which is fixed. Such a definition does not fit well with applications that process structured data like XML and JSON documents. This paper revisits the PT concepts to accommodate hierarchical data structures. The choices and pairs are created by considering the multiplicity of data instances, their access paths and common ancestors. The revised PT approach is implemented on top of on a recent data generation tool, TAF. TAF mixes random sampling and constraint solving to produce diverse data from XML-based models. Our PT implementation interacts with TAF by inserting pair coverage constraints into the models. It monitors overall coverage progress by XPath queries on the data returned by TAF. The approach is demonstrated for two data models: a 3D scene for an agricultural robot, and a population of taxpayers for a tax management system.

The optimization of regression testing (RT) has been widely studied in the literature, and numerous methods exist. However, each context is unique. Therefore, how to tell which method is appropriate for a specific industrial context? Recent work has proposed a taxonomy to aid in answering this question. The approach is to map both the RT problem and existing solutions onto the taxonomy, aiming to determine which solutions are best aligned with the problem. This paper presents a case study that evaluates the approach in a real setting. The context is the development of R&D projects at a major automotive company, in the domain of connected vehicles. We used the taxonomy to characterize the RT problem in terms of measurable effects, and to identify the technically feasible solutions from a set of 52 papers. We report on the beneficial aspects but also the difficulties of the approach, due to unclear taxonomy elements, missing ones and paper classification errors.

Field-testing is costly and time-consuming, hence, simulation-based testing is becoming more and more important to validate autonomous systems. Since autonomous systems can be deployed in diverse environments, a significant amount of diversified test cases has to be created. TAF (Testing Automation Framework) is a test generation tool we developed to serve this purpose. It produces the test cases from a data model that specifies the virtual environments of interest. This paper presents a practitioner's view of the integration of TAF into simulation-based test platforms, through two industrial case studies. The first one is for testing an agricultural robot developed by Naio Technologies, and the second one for a static perception system by SICK AG that surveils a road crossing to support connected vehicles with tracking data in complex urban scenarios. We report on our experience in the design of the data models, as well as in the automation of the execution, logging, and analysis of the generated tests. We conclude with lessons learned.

Testing in virtual road environments is a widespread approach to validate advanced driver assistance systems (ADAS). A number of automated strategies have been proposed to explore dangerous scenarios, like search-based strategies guided by fitness functions. However, such strategies are likely to produce many uninteresting scenarios, representing so extreme driving situations that fatal accidents are unavoidable irrespective of the action of the ADAS. We propose leveraging datasets from real drives to better align the virtual scenarios to reasonable ones. The alignment is based on a simple distance metric that relates the virtual scenario parameters to the real data. We demonstrate the use of this metric for testing an autonomous emergency braking (AEB) system, taking the highD dataset as a reference for normal situations. We show how search-based testing quickly converges toward very distant scenarios that do not bring much insight into the AEB performance. We then provide an example of a distance-aware strategy that searches for less extreme scenarios that the AEB cannot overcome.

Testing perception functions for safety-critical autonomous systems is a crucial task. The reason is that accurate machine learning (ML) models applied in computer vision tasks still fail in scenarios where humans perform well. Out-of-distribution (OOD) images are usually a source of such failures. For this reason, literature usually applies data augmentation techniques or runtime monitors such as OOD detectors to increase robustness. Evaluating such solutions is usually performed by analyzing metrics based on positive and negative rates over a dataset containing several perturbations. However, using such metrics on such datasets can be misleading since not all OOD data lead to failures in the perception system. Hence, testing a perception system cannot be reduced to measuring ML performances on a dataset but rely on the images captured by the system at runtime. However, the amount of time spent to generate diverse test cases during a simulation of perception components can grow quickly since it is a combinatorial optimization problem. Aiming to provide a solution for this challenging task, we present SiMOOD, an evolutionary simulation testing of safety-critical perception systems, which comes integrated into the CARLA simulator. Unlike related works that simulate scenarios that raise failures for control or specific perception problems such as adversarial and novelty, we provide an approach that finds the most relevant OOD perturbations that can lead to hazards in safety-critical perception systems. Moreover, our approach can decrease, at least ten times, the amount of time to find a set of hazards in safety-critical scenarios such as autonomous emergency braking system simulation. Besides, code is publicly available for use.

A number of simulation platforms allow the validation of advanced driver assistance systems (ADAS) in virtual road environments. However, the development of virtual tests on top of such platforms may face technical issues. Some are related to the management of the modular and configurable architecture of the simulators. Others come from the physical aspects of the simulation. Also, time and concurrency issues may affect the control of dynamic scenarios. This paper shares our experience with the virtual testing of ADAS during a period of time of more than one year. The technical issues yielded simulation crashes, ill-controlled test executions, incorrect verdict assignments, and caused a waste of time in the running and analysis of useless tests. We discuss the issues and provide recommendations for the practitioners.

High-accurate machine learning (ML) image classifiers cannot guarantee that they will not fail at operation. Thus, their deployment in safety-critical applications such as autonomous vehicles is still an open issue. The use of fault tolerance mechanisms such as safety monitors is a promising direction to keep the system in a safe state despite errors of the ML classifier. As the prediction from the ML is the core information directly impacting safety, many works are focusing on monitoring the ML model itself. Checking the efficiency of such monitors in the context of safety-critical applications is thus a significant challenge. Therefore, this paper aims at establishing a baseline framework for benchmarking monitors for ML image classifiers. Furthermore, we propose a framework covering the entire pipeline, from data generation to evaluation. Our approach measures monitor performance with a broader set of metrics than usually proposed in the literature. Moreover, we benchmark three different monitor approaches in 79 benchmark datasets containing five categories of out-of-distribution data for image classifiers: class novelty, noise, anomalies, distributional shifts, and adversarial attacks. Our results indicate that these monitors are no more accurate than a random monitor. We also release the code of all experiments for reproducibility.

The generation of test cases may have to accommodate size-varying data structures and semantic constraints between the data elements. This often requires the development of custom generators. In this paper, we introduce a novel generic tool to generate constrained and diverse test cases from a data model. First, the user defines the model using an XML-based domain-specific language. Then TAF generates diverse test cases by combining random sampling with the use of an SMT solver. The capabilities of the tool are demonstrated by four examples of models coming from various application domains: virtual crop fields for testing an agriculture robot, bitmap images with a graduated background, a population of taxpayers in a tax management system, and tree structures of diverse sizes and heights. We show how TAF performs in terms of data diversity and execution time. We also provide some comparison results with an UML-based tool using SMT solving.

Emerging high assurance solutions for safe, secure, and reliable software systemsThis editorial introduces the special issue on High Assurance Systems Engineering concepts for safe, secure, and reliable software systems in the Journal of Software: Evolution and Process.The nine papers published in this special issue were selected from extended versions of papers presented at the 2016 IEEE International Symposium on High Assurance Systems Engineering (HASE 2016) held in Orlando, Florida, through a highly competitive review process.The papers propose and discuss emerging solutions that address at least one of the three characteristics identified as foundational requirements to design, verify, and operate contemporary high assurance software systems: safety, security, and reliability, though, several papers consider a combination of these requirements, by modeling software system dependability and/or system resilience in the face of operational changes.The modeling aspects of the papers include fault-tolerant design and analysis, online logic adaptation, decision and risk analysis, malware detection, and disaster management solutions, as well as several formalized testing and verification techniques.The first paper "Systems-of-systems modeling using a comprehensive viewpoint-based SysML profile" by Marco Mori et al. addresses the design of Systems-of-Systems (SoS).The authors define a SysML profile that captures SoS concepts according to seven viewpoints like structure, evolution, dependability, and security.A smart grid use case illustrates the application of the profile to support SoS modeling and analysis.Adaptive fault tolerance is employed by Lauer et al. for maintaining dependability requirements in the face of operational and environment changes, in the framework of the Robot Operating System (ROS).Their paper "Resilient computing on ROS using adaptive fault tolerance" considers resilient embedded systems that must comply with stringent dependability requirements.Both the architecture and the actual adaptation of the proposed fault tolerance mechanisms are considered for ROS-based systems.The implementation of the proposed mechanisms shows the capability to dynamically adapt during online operations and maintain control over the components.Cyber-physical systems (CPS) operations in changing environments are also the topic of the next paper "Online verification in cyber physical systems: Practical bounds for meaningful temporal costs" authored by Marcello Bersani and Marisol Garcia-Valls.They emphasize the CPS operational adaptation through online verification of adaptation system logic.A dynamic virtualized server system operating on a dense temporal logic is considered as case study, where its mobile clients require changes in both the running components and the services executed by the server.In the fourth paper "Managing risk in high assurance systems by optimizing topological resources," Paul Hyden et al. explore novel adaptive security management strategies in the context of software defined networks or cognitive radios.They establish a process to manipulate network topology in order to minimize the risk of attacks.The process uses hop distance to separate threatening and threatened nodes, that is, it increases the security by augmenting the hop distance between such nodes.Also pertaining to security, the paper "Protecting Internet users from becoming victimized attackers of click-fraud" by Md Shahrear Iqbal et al.addresses the detection of malware for conducting click fraud.This type of malware infects a victim user's machine to produce fake clicks on ads, thereby generating fraudulent charges for online advertisers.While click-fraud protection systems are usually installed on the server side, the solution developed by the authors is on the client side, allowing users to detect and block the malicious traffic from their machine.The solution works for both desktop and mobile device systems.In their paper "Labelling relevant events to support the crisis management operator," Tommaso Zoppi et al. propose an approach to process and filter the information collected in crisis situations.The approach is integrated into a crisis management system and demonstrated on historical data from three real situations in Italy (Europa League Match, Political Manifestation, and Weather Warnings).The data comes from sources like social media, dedicated apps, websites, and sensor networks available in the infrastructures.The analysis has to cope with the heterogeneity of the sources and with integrity problems in the collected data.Ngo and Legay consider the use of statistical model checking analysis carried out directly from large SystemC models.Their paper "Formal verification of probabilistic SystemC models with statistical model checking" utilizes embedded systems as a solution to address the state space explosion common with probabilistic model checking.Bounded temporal properties for SystemC models, with both timed and probabilistic characteristics, are expressed as Bounded Linear Temporal Logic (BLTL) and verified through the implementation of the statistical model checker.The developed model also allows users to expose a rich set of user-code primitives in the form of lower level propositions in BLTL.Fei et al. propose a formal comparison between Pthreads and Dthreads, which uses the C. A. R. Hoare's Communicating Sequential Processes (CSP) approach for specifying API functions.Their paper "Comparative modeling and verification of Pthreads and Dthreads" considers four classical

Safety-critical systems with decisional abilities, such as autonomous robots, are about to enter our everyday life. Nevertheless, confidence in their behavior is still limited, particularly regarding safety. Considering the variety of hazards that can affect these systems, many techniques might be used to increase their safety. Among them, active safety monitors are a means to maintain the system safety in spite of faults or adverse situations. The specification of the safety rules implemented in such devices is of crucial importance, but has been hardly explored so far. In this paper, we propose a complete framework for the generation of these safety rules based on the concept of safety margin. The approach starts from a hazard analysis, and uses formal verification techniques to automatically synthesize the safety rules. It has been successfully applied to an industrial use case, a mobile manipulator robot for co-working.

The ability to navigate in diverse and previously unknown environments is a critical service of autonomous robots. The validation of the navigation software typically involves test campaigns in the field, which are costly and potentially risky for the robot itself or its environment. An alternative approach is to perform simulation-based testing, by immersing the software in virtual worlds. A question is then whether the bugs revealed in real worlds can also be found in simulation. The paper reports on an exploratory study of bugs in an academic software for outdoor robots navigation. The detailed analysis of the triggers and effects of these bugs shows that most of them can be revealed in low-fidelity simulation. It also provides insights into interesting navigation scenarios to test as well as into how to address the test oracle problem.

We consider lightweight usage of model-checking for the debugging of Simulink models. A problem is that model-checkers typically return only one counterexample, which may slow down the debugging process. We propose an approach and a tool to produce several counterexamples, exemplifying different property violation patterns for a given version of the design. The approach uses data collected during the replay of the counterexamples to synthesize queries for the model-checker, so that it finds counterexamples that activate new paths. The approach is applied to an academic example and an industrial model from the automotive domain.

Statistical testing is a probabilistic approach to test data generation that has been demonstrated to be very effective at revealing faults. Its premise is to compensate for the imperfect connection between coverage criteria and the faults to be revealed by exercising each coverage element several times with different random data. The cornerstone of the approach is the often complex task of determining a suitable input profile, and recent work has shown that automated metaheuristic search can be a practical method of synthesising such profiles. The starting point of this paper is the hypothesis that, for some software, the existing grammar-based representation used by the search algorithm fails to capture important relationships between input arguments and this can limit the fault-revealing power of the synthesised profiles. We provide evidence in support of this hypothesis, and propose a solution in which the user provides some basic contextual knowledge to guide the search. Empirical results for two case studies are promising: knowledge gained by a very straightforward review of the software-under-test is sufficient to dramatically increase the efficacy of the profiles synthesised by search.

In this paper we present STELAE, a model-driven test development environment for avionics embedded systems, implemented on top of a real integration test platform. It is the result of an R&D project between two research laboratories and a test solution provider, aiming to introduce model-driven engineering methodologies and technologies for the development of tests. Our work was motivated by the multiplicity of proprietary test languages in this industrial context, which no longer respond to the stakeholder needs. We present the early prototype functionalities (test model definition, automatic code generation and execution) on a case study inspired from real-life. Our feedback on the used technologies concludes this paper.

Tests for avionics embedded systems are implemented using proprietary test languages. No standard has emerged and the set of existing test languages is heterogeneous. This is challenging for test solution providers, who have to accommodate the different habits of their clients. In addition, test exchange between aircraft manufacturers and equipment/system providers is hindered. To address these problems, we propose a model-driven approach for test implementation: test models are developed/maintained, with model-tocode transformations towards target executable test languages. This paper presents the test meta-model underlying the approach. It integrates the domain-specific concepts identified from an analysis of a sample of proprietary test languages. The test meta-model is the basis for building test model editors and templatebased automatic code generators, as illustrated by a demonstrator we developed.

Mobile computing systems provide new challenges for verification. One of them is the dynamicity of the system structure, with mobility-induced connections and disconnections, dynamic creation and shutdown of nodes. Interaction scenarios have then to consider the spatial configuration of the nodes as a first class concept. This paper presents GraphSeq, a graph matching tool for sequences of configurations developed in the framework of testing research. It aims to analyze test traces to identify occurrences of the successive spatial configurations described in an abstract scenario. We present the GraphSeq algorithm, as well as first experiments using randomly generated graphs, outputs from a mobility simulator, and test traces from a case study in ad hoc networks.

Advances in wireless networking have yielded the development of mobile applications. However, sound technology to specify, design and validate such applications is still to be investigated. In order to exemplify some of the challenges that are raised, this paper reports on a case study: a group membership protocol for ad hoc networks. The protocol has been analyzed by reviewing the specification and the code, and then by testing the implementation. The outcomes provides us with hints for research direction.

Proof-guided testing is intended to enhance the test design with information extracted from the argument for correctness. The target application field is the verification of fault-tolerance algorithms where a paper proof is published Ideally, testing should be focused on the weak parts of the demonstration. The identification of weak parts proceeds by restructuring the informal discourse as a proof tree and analyzing it step by step. The approach is experimentally assessed using the example of a flawed group membership protocol (GMP). Results are quite promising: (1) compared to crude random testing, the proof-guided method allowed us to significantly improve the fault revealing power of test data; (2) the overall method also provided useful feedback on the proof and its potential flaw(s).

Proof-guided testing is intended to enhance the test design with information extracted from the argument for correctness. The target application field is the verification of fault-tolerance algorithms where a complete formal proof is not available. Ideally, testing should be focused on the pending parts of the proof. The approach is experimentally assessed using the example of a group membership protocol (GMP), a complete proof of which has been developed by others in the PVS environment. In order to obtain a partial proof example, we proceed to flaw insertion into the PVS specification. Test selection criteria are then derived from the analysis of the reconstructed (now partial) proof. Their efficiency for revealing the flaw is experimentally assessed, yielding encouraging results.

This paper aims at verifying properties of generic fault-tolerance algorithms. Our goal is to enhance the testing process with information extracted from the proof of the algorithm, whether this proof is formal or informal: ideally, testing is intended to focus on the weak parts of the proof (e.g., unproved lemmas or doubtful informal evidence). We use the Fault-Tolerant Rate Monotonic Scheduling algorithm as a case study. This algorithm was proven by informal demonstration, but two faults were revealed afterwards. In this paper, we focus on the analysis of the informal proof, which we restructure in a semiformal proof tree based on natural deduction. From this proof tree, we extract several functional cases and use them for testing a prototype of the algorithm. Experimental results show that a flawed informal proof does not necessarily provide relevant information for testing. It remains to investigate whether formal (partial) proofs allow better connection with potential faults.

One of the characteristics of object-oriented software is the complex dependency that may exist between classes due to inheritance, association and aggregation relationships. Hence, where to start testing and how to define an integration strategy are issues that require further investigation. This paper presents an approach to define a test order by exploiting a model produced during design stages (e.g., using OMT, UML), namely the class diagram. Our goal is to minimize the number of stubs to be constructed in order to decrease the cost of testing. This is done by testing a class after the classes it depends on. The novelty of the test order lies in the fact that it takes account of: (i) dynamic (polymorphism) dependencies; (ii) abstract classes that cannot be instantiated, making some testing levels infeasible. The test order is represented by a graph showing which testing levels must be done in sequence and which ones may be done independently. It also provides information about the classes involved in each level and how they are involved (e.g., instantiation or not). The approach is implemented in a tool called TOONS (Testing level generator for Object-OrieNted Software). It is applied to an industrial case study from the avionics domain.

The B method is a model-based approach covering all the software development process, from the specification to the code. External verification of B models aims to determine whether they correctly capture the informal requirements. It is argued that verification techniques like B model animation or code testing should accompany the formal development process and give a feedback of the system that is actually being specified. A uniform testing framework, irrespective of whether the input cases are executed on the final code or on the formal models, is presented. A B development process is considered as a series of stages where concrete models are built gradually based on the more abstract ones, the final code being just a compiled version of the most concrete model. A definition of test correctness, related to the one of refinement, is introduced. The consequences in terms of required animation facilities are discussed.

Specification in B: An Introduction described with first-order logic and a set-theoretic model, while the dynamics (operations) are Using the B Toolkit.Kevin Lano and Howard Haughton.Published by Imperial Col-expressed by means of generalized substitutions having the semantics of predicate transformers.lege

The B method is a formal approach covering all the software development process, through a series of proved refinement steps. An on going debate in the B community is the removal of some classical verification steps of the design, eg. unit and integration testing: the paper is aimed to support the maintenance of stringent testing policies. We first recall previous work that addresses the general question of the limits of formal methods for ultra high dependability (A. Cohn, 1989; A. Hall, 1990). Then, the discussion is focused on the case of the B method. Although the method significantly contributes to fault avoidance, it is shown that additional verifications are still required throughout the development process, whether inspections or tests.

This paper is concerned with the use of statistical testing as a verification technique for complex software. Statistical testing involves exercising a program with random inputs, the test profile and the number of generated inputs being determined according to criteria based on program structure or software functionality. In case of complex programs, the probabilistic generation must be based on a black box analysis, the adopted criteria being defined from behavior models deduced from the specification. The proposed approach refers to a hierarchical specification produced in the STATEMATE environment. Its feasiblity is exemplified on a safety-critical module from the nuclear field, and the efficiency in revealing actual faults is investigated through experiments involving two versions of the module.