Lina Marsso, Radu Mateescu, Lucie Muller, Wendelin Serwe
Abstract: We present two behavioral models of an autonomous vehicle and its interaction with the environment. Both models use the formal modeling language LNT provided by the CADP toolbox. This paper discusses the modeling choices and the challenges of our autonomous vehicle models, and also illustrates how formal validation tools can be applied to a single component or the overall vehicle.
Endri Kaja, Nicolas Gerlin, Mounika Vaddeboina, Luis Rivas, Sebastian Prebeck, Zhao Han, Keerthikumara Devarajegowda, Wolfgang Ecker
Abstract: Safety-critical designs used in automotive applications need to ensure reliable operations even under hostile operating conditions. As these designs grow in size and complexity, they are facing an increased risk of failure. Consequently, the methods applied to validate the reliability of designs require increasingly more compute resources (e.g., fault simulation time) and manual efforts. Rigorous and highly automated safety analysis methods are needed to cope with this rising complexity. In this paper, we propose a model-based safety analysis flow to enable fault injection at different abstraction levels of a design. The fault simulation is performed at register transfer level (RTL) of a design, in which parts of the design targeted for fault simulation are represented with gate-level granularity. This mixed representation of a design provides a significant rise in fault simulation performance while maintaining the same accuracy as a gate-level fault simulation. To demonstrate the applicability of the proposed approach, various RISC- V based CPU subsystems that are part of automotive SoCs are considered for fault simulation. The experimental results show an increase of 3.5x - 8.4x in the fault simulation performance with substantially less manual effort as all the design activities are automated utilizing a model-driven RTL generation flow.
Jean-Baptiste Horel, Christian Laugier, Lina Marsso, Radu Mateescu, Lucie Muller, Anshul Paigwar, Alessandro Renzaglia, Wendelin Serwe
Abstract: Simulation, a common practice to evaluate au-tonomous vehicles, requires to specify realistic scenarios, in par-ticular critical ones, occurring rarely and potentially dangerous to reproduce on the road. Such scenarios may be either generated randomly, or specified manually. Randomly generating scenarios is easy, but their relevance might be difficult to assess. Manually specified scenarios can focus on a given feature, but their design might be difficult and time-consuming, especially to achieve satisfactory coverage. In this work, we propose an automatic approach to generate a large number of relevant critical scenarios for autonomous driving simulators. The approach is based on the generation of behavioral conformance tests from a formal model (specifying the ground truth configuration with the range of vehicle behaviors) and a test purpose (specifying the critical feature to focus on). The obtained abstract test cases cover, by construction, all possible executions exercising a given feature, and can be automatically translated into the inputs of autonomous driving simulators. We illustrate our approach by generating thousands of behavior trees for the CARLA simulator for several realistic configurations.
Ligocki, Adam, Zalud, Ludek
Abstract: This paper deals with human detection in the LiDAR data using the YOLO object detection neural network architecture. RGB-based object detection is the most studied topic in the field of neural networks and autonomous agents. However, these models are very sensitive to even minor changes in the weather or light conditions if the training data do not cover these situations. This paper proposes to use the LiDAR data as a redundant, and more condition invariant source of object detections around the autonomous agent. We used the publically available real-traffic dataset that simultaneously captures data from RGB camera and 3D LiDAR sensors during the clear-sky day and rainy night time and we aggregate the LiDAR data for a short period to increase the density of the point cloud. Later we projected these point cloud by several projection models, like pinhole camera model, cylindrical projection, and bird-view projection, into the 2D image frame, and we annotated all the images. As the main experiment, we trained the several YOLOv5 neural networks on the data captured during the day and validate the models on the mixed day and night data to study the robustness and information gain during the condition changes of the input data. The results show that the LiDAR-based models provide significantly better performance during the changed weather conditions than the RGB-based models.
Oliver A. Tazl, Franz Wotawa
Abstract: The use of Artificial Intelligence methodologies including machine learning for object recognition and other tasks as well as reasoning has recently gained more attention. This is due to the fact of applications like autonomous driving but also apps for providing recommendations or schedules. In this paper, we focus on testing applications utilizing logic theorem proving for implementing their functionalities. Testing logic theorem prover is important in order to assure that the obtained results are correct and complete as specified. We show how metamorphic testing can be used in this context. In particular, the proposed method takes a logic sentence and modifies it without changing its logical status, i.e., satisfiability. The testing method can be applied to assure the correctness of reasoning via generating logic sentences of arbitrary sizes, but also for performance testing. We applied the presented testing method to 2 different theorem provers and report on obtained results.