ABSTRACT Background Object detection modules are essential functionalities for any autonomous vehicle. However, the performance of such modules implemented using deep neural networks can be unreliable in many cases, which raises the necessity to filter the abnormal outputs for safety considerations. Aims This article aims to develop a logical framework for filtering potentially erroneous object detection results. Materials & Methods Concretely, we consider two types of abstraction, namely spatial abstraction and temporal abstraction, based on the data labels from the training dataset of object detectors, and temporal consistency between a sequence of images. Operated on the training dataset, the construction of spatial abstraction iterates each input, aggregates region‐wise information over its associated labels, and stores the object abstraction. The abstraction is adopted to filter static and spatial abnormalities. The temporal abstraction builds an abstract transformer for a relaxed tracking algorithm. Elements being associated together by the abstract transformer can be checked against consistency over their original values. The abstraction helps to monitor temporal abnormality in consecutive frames. We have implemented the overall framework and validated it using publicly available datasets and open‐source object detectors. Results The implemented framework successfully identified most of static/spatial and temporal abnormalities in object detection outputs. Validation on public datasets confirmed the effectiveness of the abstraction‐based approach in filtering unreliable detections. Discussion The results demonstrate that logical abstractions derived from training data labels and temporal sequences provide a viable mechanism for monitoring the reliability of deep neural network‐based object detectors. Conclusion Abstraction‐based monitoring presents a robust and logical framework for enhancing the reliability of object detectors by filtering abnormal detection results.

In this paper, we introduce Def-VAE, a novel adversarial defense framework based on modeling real-world data distributions with Variational Autoencoders (VAEs), which can effectively defend image classifiers against adversarial attacks.Unlike traditional adversarial training methods that need to retrain the classifier, our approach does not rely on exposure to any adversarial examples during training, nor is it constrained to defend against specific models or attack algorithms.By leveraging the VAE's capability to learn the underlying distribution of clean data, we create a robust latent representation that can identify anomalous characteristics of adversarial inputs and figure out the original classifications.Experimental results demonstrate that Def-VAE achieves high defense success rates against diverse adversarial attacks for various datasets, showing the model and attack-agnostic resilience.

Testing autonomous driving systems (ADS) presents significant challenges in trajectory planning, route control, and collision avoidance, particularly at complex junctions. Among these, irregular junctions are especially valuable for exposing ADS weaknesses—yet they remain difficult to generate systematically. Since manually configured irregular junctions may not accurately reflect real-world conditions, a more practical approach is to identify existing irregular junctions. This paper presents a method for extracting irregular junctions from global OpenStreetMap (OSM) data and generating safety-critical scenarios based on them. By analyzing junction topologies and quantifying them with a difficulty metric, our approach uncovers challenging scenarios that effectively expose ADS defects. Experimental evaluations with various autopilots show that the identified junctions and generated scenarios trigger unique ADS defects more effectively than simulator-provided ones.

We investigate a rigorous simulation and testing-based validation method for autonomous driving systems that integrates an existing industrial simulator and a formally defined testing environment. The environment includes a scenario generator that drives the simulation process and a monitor that checks at runtime the observed behavior of the system against a set of system properties to be validated. The validation method consists in extracting from the simulator a semantic model of the simulated system including a metric graph, which is a mathematical model of the environment in which the vehicles of the system evolve. The monitor can verify properties formalized in a first-order linear temporal logic and provide diagnostics explaining their non-satisfaction. Instead of exploring the system behavior randomly as many simulators do, we propose a method to systematically generate sets of scenarios that cover potentially risky situations, especially for different types of junctions where specific traffic rules must be respected. We show that the systematic exploration of risky situations has uncovered many flaws in the real simulator that would have been very difficult to discover by a random exploration process.

ComOpT is an open-source research tool for coverage-driven testing of autonomous driving systems, focusing on planning and control. Starting with (i) a meta-model characterizing discrete conditions to be considered and (ii) constraints specifying the impossibility of certain combinations, ComOpT first generates constraint-feasible abstract scenarios while maximally increasing the coverage of k-way combinatorial testing. Each abstract scenario can be viewed as a conceptual equivalence class, which is then instantiated into multiple concrete scenarios by (1) randomly picking one local map that fulfills the specified geographical condition, and (2) assigning all actors accordingly with parameters within the range. Finally, ComOpT evaluates each concrete scenario against a set of KPIs and performs local scenario variation via spawning a new agent that might lead to a collision at designated points. We use ComOpT to test the Apollo 6 autonomous driving software stack. ComOpT can generate highly diversified scenarios with limited test budgets while uncovering problematic situations such as inabilities to make simple right turns, uncomfortable accelerations, and dangerous driving patterns. ComOpT participated in the 2021 IEEE AI Autonomous Vehicle Testing Challenge and won first place among more than 110 contending teams.

As bugs of Python built-in types can cause code crashes, detecting them is critical to the robustness of the software. Researchers have concluded plenty of patterns for the bug causes and applied these patterns in detection tools. But these tools are only evaluated on handcrafted bugs or bugs obtained from QA pages. Because such bugs cannot reflect the complex code structures and various bug types encountered in real-world projects, the evaluation result is untrustworthy when applied to these projects. As a result, a collection of real-world reproducible bugs is essential for tool evaluation and future bug-related research. In this paper, we propose ExcePy, a benchmark for providing bugs of Python built-in types. We collect 180 bugs from the evolution of 15 real-world open-source Python projects on GitHub and then manually build test scripts for bug reproduction. Meanwhile, to improve tool evaluation efficiency, we present a code pruning strategy that can minimize buggy code size while retaining bug reproducibility and apply it to ExcePy to provide simplified buggy code. To demonstrate the benefits of ExcePy, we use three static analyzers and two fuzzers to detect bugs collected in ExcePy. We found that simplified code can significantly reduce running time and avoid many tool crashes, and bugs supplied by ExcePy can reveal limitations of existing tools in reporting real-world bugs.

Deploying deep neural networks (DNNs) as core functions in autonomous driving creates unique verification and validation challenges.In particular, the continuous engineering paradigm of gradually perfecting a DNN-based perception can make the previously established result of safety verification no longer valid.This can occur either due to the newly encountered examples (i.e., input domain enlargement) inside the Operational Design Domain or due to the subsequent parameter fine-tuning activities of a DNN.This paper considers approaches to transfer results established in the previous DNN safety verification problem to the modified problem setting.By considering the reuse of state abstractions, network abstractions, and Lipschitz constants, we develop several sufficient conditions that only require formally analyzing a small part of the DNN in the new problem.The overall concept is evaluated in a 1/10-scaled vehicle that equips a DNN controller to determine the visual waypoint from the perceived image.

While object detection modules are essential functionalities for any autonomous vehicle, the performance of such modules that are implemented using deep neural networks can be, in many cases, unreliable. In this paper, we develop abstraction-based monitoring as a logical framework for filtering potentially erroneous detection results. Concretely, we consider two types of abstraction, namely data-label abstraction and post-algorithm abstraction. Operated on the training dataset, the construction of data-label abstraction iterates each input, aggregates region-wise information over its associated labels, and stores the vector under a finite history length. Post-algorithm abstraction builds an abstract transformer for the tracking algorithm. Elements being associated together by the abstract transformer can be checked against consistency over their original values. We have implemented the overall framework to a research prototype and validated it using publicly available object detection datasets.

Energy optimization plays an increasingly critical role in designing an embedded real-time multiprocessor System on Chip (MPSoC). Dynamic Voltage Frequency Scaling (DVFS) and Dynamic Power Management (DPM) are preferable techniques to optimize energy consumption. However, previous DVFS and DPM algorithms were mostly designed for inter-task scheduling, without sufficient exploration on intra-task scheduling for further energy reduction. This paper presents a new intra-task scheduling approach considering the probabilistic distribution of task execution time, and it optimizes the mathematical expectation of power consumption (expected power consumption) for periodic dependent tasks with uncertain execution time running on MPSoCs using DVFS and DPM. The energy-efficient scheduling problem can be formulated by means of mixed integer linear programming (MILP) with the proposed technique. Moreover, we also propose a technique to compress the exploration space by reorganizing the probabilistic profiling information of all tasks. Our experimental results on synthetic and realistic benchmarks show that the proposed approach achieves up to 30 percent energy savings compared with other existing methods.

We consider spacial and temporal aspects of communication to avoid contention in Network-on-Chip (NoC) architectures. A constraint model is constructed such that the design concerns can be evaluated, and an efficient evolutionary algorithm with various heuristics is proposed to search for better solutions. Experimentations from random benchmarks demonstrate the efficiency of our method in multi-objective optimization and the effectiveness of our techniques in avoiding network contention.

Deep neural networks (DNNs) have been increasingly adopted in various applications. Systematic verification and validation is essential to guarantee the quality of such systems. Due to the scalability problem, formal methods can hardly be widely applied in practice. Testing is one of feasible solutions. However, lacking of input space specification for DNNs requires a large set of test cases to be constructed to increase the testing adequacy, which leads to high labeling cost of test cases. In this paper, we put forwards a test case prioritization method for DNN classifiers, which assigns high priorities to those cases that could lead to wrong classifications. The priorities are calculated according to the activation pattern of neurons acquired from the training sets and the activated neurons collected from certain inputs. For a trained model, the method consists of two steps. First, we accumulate neuron activation patterns over the training set, and construct a set of frequently activated neurons based on the frequency (times) of activation for every class. Second, the metrics are computed according to the comparison between the activated neurons of an input and the selected set of frequently activated neurons with its output. The experimentation is carried out over three popular datasets with various neural network structures. The results demonstrate that the test cases with higher priorities are more prone to be mis-classified. And the prioritized test cases over a DNN model within same datasets are also efficient in triggering mis-classification of other DNNs with similar structures.

Network-on-Chip (NoC) is a promising interconnecting paradigm in the state-of-the-art multi-core architectures. Its communication network can increase the capacity of parallel data transfer such that system performance is improved. In the design of MPSoC-based applications, multiple objectives exist, such as minimizing time and energy consumption, which may conflict and certain trade-off needs to be evaluated. Heuristic-based methods such as evolutionary algorithms are always adopted to find near-optimal solutions for such applications. However, it is hard to evaluate the accuracy of those solutions. As most of the constraints on the mapping and scheduling process of NoCs can be described as logic formulas, we apply SMT-based methods for the multi-objective optimization of NoC-based MPSoCs. Moreover, to improve the scalability of the optimization problem, we propose to reduce the search space with respect to the symmetry feature of NoC architecture, and to decompose the search process according to the feature of non-dominated solutions. Extensive experimental results from random and real-case benchmarks demonstrate the accuracy of SMT-based methods in finding all the Pareto-fronts, and the efficiency of the proposed strategies.

Providing guarantees on the system behavior is mandatory for safety-critical autonomous vehicles. Among these guarantees, proving the fulfillment of real-time constraints and reliability requirements on the system is a key issue, as their violation could result in unexpected and unsafe behaviors. The violation may come from the complicated interaction between software and hardware modules, or transient hardware faults. AUTOSAR, the most popular industrial standard in the automotive domain, provides an open standardized architecture for software development, where an application can be deployed on multiple electronic control units (ECUs). We present a verification and validation method for the design of such safety-critical autonomous control systems that could tolerate transient faults. The embedded implementation of an AUTOSAR model is transformed into a three-layer system model in timed automata, so that system behavior can be evaluated and checked with hard real-time constraints and the implementing architecture. We demonstrate the feasibility of the method with a simplified controller developed for the autonomous vehicles.

Equipped with customized parameters, configurable software is more flexible when facing various hardware platforms and scenario options. The configurability can tailor the source code to different instances. Consequently, it is difficult for developers to enumerate all possible configurations for finding bugs, especially for large-scale configurable software systems. In this paper, we propose a method to efficiently detect bugs of such systems with static analysis techniques. The method takes advantage of combinatorial testing techniques to generate sufficient configurations. It first extracts required parameters and the corresponding constraints from a configure file. The parameters together with constraints are employed to generate configurations with required coverage. Considering the features of configuration options, we further classify the parameters into clusters, according to the tightness of their relations. Inspired from the idea of divide-and-conquer, every cluster can be assigned with a local strength, such that the tightly coupled options can be covered, without incurring other unnecessary options. Such improvement can reduce the number of required configurations, thus improving the efficiency of static analysis. The experimental results over four real-world configurable systems demonstrate the efficiency, scalability and practicality of our method.

MPSoCs are increasingly being adopted in the design of emerging complex embedded systems. Resource limitations require designers to find optimizations among various design considerations. Task mapping and scheduling become one of the key issues in designing such systems. To meet the requirements of makespan minimization and workload balance for energy-aware MPSoCs, the paper presents a unified formulation to find satisfied task mapping and scheduling solutions. The model considers both computation and communication cost, and enables applying dynamic power management (DPM) for energy optimization. To efficiently approximate the Pareto front of the optimization problem, we propose a multi-objective hybrid algorithm (MOHA) by integrating a Pareto local search into an evolutionary process, with a problem-specific initialization. Experimental results from realistic benchmarks demonstrate that the proposed techniques are able to generate high-quality solutions of realistic applications on the target architecture, compared with state-of-the-art methods.

Communication frequency is increasing with the growing complexity of emerging embedded applications and the number of processors in the implemented multiprocessor SoC architectures. In this article, we consider the issue of communication cost reduction during multithreaded code generation from partitioned Simulink models to help designers in code optimization to improve system performance. We first propose a technique combining message aggregation and communication pipeline methods, which groups communications with the same destinations and sources and parallelizes communication and computation tasks. We also present a method to apply static analysis and dynamic emulation for efficient communication buffer allocation to further reduce synchronization cost and increase processor utilization. The existing cyclic dependency in the mapped model may hinder the effectiveness of the two techniques. We further propose a set of optimizations involving repartition with strongly connected threads to maximize the degree of communication reduction and preprocessing strategies with available delays in the model to reduce the number of communication channels that cannot be optimized. Experimental results demonstrate the advantages of the proposed optimizations with 11--143% throughput improvement.

To accelerate the speed of performance estimation and raise its accuracy for MPSoC, we propose a static analysis and dynamic annotation combined method to efficiently model cache mechanism in native simulation. We use a new cache model to statically analyze segmental profiling results to speed up simulation, and utilize a dynamic annotation technique to exactly trace the addresses of local variables. Experimental results show the efficiency of the proposed techniques for more accurate system performance estimation.

Context-based adaptive binary arithmetic coding (CABAC) is the major entropy-coding algorithm employed in H.264/AVC. In this paper, we present a new VLSI architecture design for an H.264/AVC CABAC decoder, which optimizes both decode decision and decode bypass engines for high throughput, and improves context model allocation for efficient external memory access. Based on the fact that the most possible symbol (MPS) branch is much simpler than the least possible symbol (LPS) branch, a newly organized decode decision engine consisting of two serially concatenated MPS branches and one LPS branch is proposed to achieve better parallelism at lower timing path cost. A look-ahead context index (ctxIdx) calculation mechanism is designed to provide the context model for the second MPS branch. A head-zero detector is proposed to improve the performance of the decode bypass engine according to UEG k encoding features. In addition, to lower the frequency of memory access, we reorganize the context models in external memory and use three circular buffers to cache the context models, neighboring information, and bit stream, respectively. A pre-fetching mechanism with a prediction scheme is adopted to load the corresponding content to a circular buffer to hide external memory latency. Experimental results show that our design can operate at 250 MHz with a 20.71k gate count in SMIC18 silicon technology, and that it achieves an average data decoding rate of 1.5 bins/cycle.

Efficient design of multiprocessor system-on-chip (MPSoC) requires early, fast, and accurate performance estimation techniques. In this paper, we present new techniques based on fine-grained code analysis to estimate accurate performance during simulation of MPSoC transaction accurate models. First, a GCC profiling tool is applied in the native simulation process. Based on the profiling result, an instruction analyzer of the target CPU architecture is proposed to analyze the cycle cost of C code under estimation. In addition, a memory analyzer is used to further estimate memory access latency including both instruction/data cache time cost and global memory access cycles. Both data and instruction cache models are proposed to estimate cache miss penalty, and a segment-based strategy is adopted to update the cache models more efficiently. Furthermore, an equalized access model is presented to imitate the memory access behavior of processors for estimating global memory access latency caused by bus contention and memory bandwidth. We have applied these techniques on an H.264 decoder application with different hardware architectures. The experimental results show that applying these techniques can obviously improve estimation accuracy of transaction accurate models close to that of the virtual prototype models, with a tolerable overhead on simulation speed.

We consider a compositional method for the verification of component-based systems described in a subset of the BIP language encompassing multi-party interactions. The method is based on the use of two kinds of invariants. Component invariants are over-approximations of components' reach ability sets. Interaction invariants are constraints on the states of components involved in interactions. In this paper we propose fixed point characterization for computing interaction invariants. We also propose a new technique that takes the incremental design of the system into account. In many situations, the technique will help to avoid redoing all the verification process each time an interaction is added in the design. Our two techniques have been implemented as extension of the D-Finder toolset. The result has been applied to check deadlock-freedom on several case studies. Our experiments show that our new methodology is generally much faster than existing ones.