CommonUppRoad: A Framework of Formal Modelling, Verifying, Learning, and Testing of Autonomous Vehicles

Rong Gu⁺ , Kaige Tan^# , Andreas Holck Høeg-Petersen* , Lei Feng^#, Kim Guldstrand Larsen*

⁺Mälardalen University, Sweden. ^#KTH, Sweden. *Aalborg University, Denmark.

Combining machine learning and Formal Methods (FMs) provides a possible solution to overcome the safety issue of Autonomous Driving (AD) vehicles. However, there are gaps to be bridged before this combination becomes practically applicable and useful. In an attempt to facilitate researchers in both FMs and AD areas, this study aims to propose a framework that combines two well-known tools, namely CommonRoad and UPPAAL. On the one hand, CommonRoad can be enhanced by the rigorous semantics of models in UPPAAL, which enables a systematic and comprehensive understanding of the AD system’s behaviour and thus strengthens the safety of the system. On the other hand, controllers synthesised by UPPAAL can be visualised by CommonRoad in real-world road networks, which facilitates AD vehicle designers greatly adopting formal models in system design. In this framework, we provide automatic model conversions between CommonRoad and UPPAAL. Therefore, users only need to program in Python and the framework takes care of the formal models, learning, and verification in the backend.
CommonUppRoad has been published lately¹ . Users can easily configure their motion planning environment and vehicle parameters in the Python program, and the framework generates UPPAAL models for them. Using these models, one can run simulation and model checking to decide a suitable period of decision making. One can also check the existence of valid motion plans before running reinforcement learning. These steps are called “model pre-analysis” in this study, which is automated in the framework and has been proven to be useful facilitating reinforcement learning in the next stage.
After the model pre-analysis, one can start motion planning by synthesizing a safety shield first. This safety shield is the so-called permissive strategy in the UPPAAL literature, which contains all actions as long as they keep the AD vehicle safe. Next, one can run reinforcement learning under the control of the safety shield, i.e., the random simulation of an AD vehicle is within the reachable set of the safety shield. In this way, the learning process as well as the result are guaranteed to be safe. In addition, learning can be accelerated because the safety shield has eliminated meaningless actions. An ongoing work on CommonUppRoad is scenario generation. While motion planning focuses on the AD vehicle, scenario generation is about generating trajectories of other traffic agents, such as pedestrians and vehicles. Briefly, scenario generation in CommonUppRoad can automatically parse functional scenarios (i.e., natural language description of requirements), generate logic scenarios (i.e., parameters ranges), and instantiate the logic scenarios into concrete scenarios (i.e., trajectories). Users can test their AD vehicles in these scenarios via simulations in CommonRoad or other platforms such as Esmini and Carla.

1. https://sites.google.com/view/commonupproad

INTERSTICE: INTelligent sEcuRity SoluTIons for Connected vEhicles

Mahshid Helali Moghadam

Scania CV AB, Sweden

The digital evolution of the automotive industry with the evolving in-vehicle systems, advanced driver assistance technologies, and growing connectivity introduces new cyber security risks. International regulations such as UN Regulation No. 155, require manufacturers to implement cyber security measures for threat detection, prevention, and mitigation. The threats may originate from multiple entry points, including sensors, infotainment systems, telematics units, or direct physical interfaces. They may disrupt in-vehicle networks, interfere with data transmission, and cause Electronic Control Units (ECUs) to malfunction. Onboard Intrusion Detection Systems (IDS) for in-vehicle networks, e.g., Controller Area Network (CAN) and Automotive Ethernet (AE), are essential for monitoring traffic, identifying suspicious activities, and enabling timely threat mitigation. INTERSTICE is a research initiative between Scania CV AB, RISE, and Scaleout Systems AB, which focuses on developing architecture-aware distributed machine learning driven systems for onboard IDS. The project addresses key challenges, including the scarcity of attack-representing data, intelligent cyber threat detection, onboard (ECUbased) IDS deployment, and explainable inference for ML-driven IDS solutions. INTERSTICE introduces:

• (a) innovative methods for generating attack-representing data utilizing precise parameterized attack modeling, generative AI, i.e., LLM-based agents;
• (b) distributed ML-driven solutions for detecting attacks with various disruptive mechanisms, including message fabrication (e.g., Denial of Service (DoS) and fuzzy attacks), suspension, masquerade (e.g., spoofing attack), and message replay on CAN;
• (c) strategies for the deployment of CAN IDS on vehicle ECUs, w.r.t real-world constraints, and federated learning-based solutions for developing vehicle aggregated IDS model;
• (d) attack modeling and synthetic attack generation for AE;
• (e) advanced ML-driven solutions for AE IDS.

Consolidating Model Compilation via a Middle Language

Hiep Hong Trinh*, Federico Ciccozzi, Marjan Sirjani, Mikael Sjödin, Abu Naser Masud

Mälardalen University, IDT school (Västerås, Sweden)

Code-centric development is error-prone when it comes to complex software-driven systems (like cyber-physical systems, IoT, autonomous robotics, multi-agent systems), which often contain distributed, concurrent components and interactions with the environment. Actionable software based models help to design, experiment, create and verify such systems through simulation, code generation and formal verification. Each model is an incomplete representation of the real system for some discrete purposes and there is always a need for interoperability among them. Model compilation is the process of parsing and compiling a high-level abstract model of a system defined in a formal textual language to derive other models therefrom. Due to the versatility of modeling and programming languages, a custom compiler is required for each source-target pair, which is a complex and repeated task. We therefore propose a toolchain for a reusable model compilation paradigm by introducing a pivot modelling language, namely M, which serves as a hosting language to allow adapting other modeling languages to. Modelers can also model directly on M as M itself is designed to be a versatile cross-domain modelling language. From a top model in M, the toolchain will parse it once and reuse the parse assets for all other subsequent translations to other input models of tools for simulation, code generation and verification (model-checking).
Current progress and future plans. We are designing a candidate for the M language based on the actor model and the DEVS (discrete event system specification) formalism. With the combination of asynchronous message-passing and discrete-event semantics, our M language can be used to model various systems, especially cyber-physical systems and distributed autonomous robotics, and can serve as a host language to adapt a wide range of modelling languages to. Supporting of modelling continuous or hybrid systems is also being considered as DEVS can be combined with DESS (differential equation system specification) formalism to model continuous behaviors. For the front-end language engineering tasks (syntactic parsing and semantic analysis), we intend to use ANTLR4 for grammar definition and parser generation, and JastAdd for building abstract syntax tree, which is reused for all subsequent translations. For the back-end tasks, we favor black-box uses of existing tools and platforms by adapting M to their input formats. In case such reuse is not possible we will work out our own implementation. The approach also opens opportunities of using Large-Language Models for code generation. In the next phase we will publish our works on the M language design and automatic verification of semantic equivalence. After having a prototypical release, we intend to evaluate the toolchain in several industrial contexts with our partner companies who work on robotics, smart vehicles and embedded systems.
Vision. Systems are getting more complex, model-based engineering is a way of escaping from low-level details to focus on higher-level views, helping to design and create systems faster, more predictable, more reliable. Once the toolchain is in place, adaptors can be developed to map other modelling languages to M and a semantics-aware model compilation paradigm is ready without extra custom work. The M toolchain forms a full end-to-end ecosystem of engineering tools including modelling, simulation, execution, verification without requiring the system developers to know and implement complicated mechanisms behind them other than adapting to or using M language directly.

Enhancing the Robustness of Computer Vision in Construction Environments

Maghsood Salimi

Mälardalen University, IDT school (Västerås, Sweden)

This research improves the resilience of computer vision models in challenging real-world settings, particularly construction sites, where weather conditions, sensor limitations, and adversarial attacks degrade performance. To address these challenges, we propose novel optimization frameworks—SARAF and a hybrid Simulated Annealing–Late Acceptance Hill-Climbing method—to enhance CNN robustness against adversarial attacks efficiently.
Additionally, we introduce ConstScene, a specialized dataset featuring diverse weather and environmental conditions, enabling better model training and evaluation. To further enhance adaptability while preserving data privacy, we explore Federated Learning (FL) for decentralized, continuous learning. We also leverage Few-Shot Learning (FSL) with optimized hyperparameters to enable models to quickly adapt with minimal data, reducing dependence on large datasets. These contributions collectively strengthen computer vision models against natural and adversarial perturbations while improving efficiency, making them more reliable for dynamic construction environments.

Streamlining Parameter Tuning in Full-Body Racing Simulators with an Automated Pipeline

(Best Poster Award)

Ruslan Shaiakhmetov¹, Danilo Pianini¹, Gabriele D’Angelo¹, Valter Venusti²

¹Alma Mater Studiorum – University of Bologna, ²Dallara Automobili S.p.A.

Simulation tools are essential for designing and testing car setups in modern racecar competitions. State-of-the-art full-body simulators replicate driving conditions but require detailed tuning (alignment) of hundreds or thousands of parameters to reduce the reality gap. This process, typically performed by comparing simulations with real-world data, is time-consuming, requires advanced expertise, and relies on human intuition. As a result, alignment outcomes are highly subjective and may vary depending on the engineer performing the operation.
To address these challenges, we propose an automated pipeline for parameter tuning in full-body racing simulators. This pipeline replicates the manual tuning workflow, substituting subjective visual comparisons with an objective cost function based on the Residual Sum of Squares (RSS). Our approach stems from an analysis of existing best practices to identify sources of variability and opportunities for improvement. The main limitation of current methods arises from human factors and the complexity of parameter interactions. By leveraging automation, the proposed pipeline enhances the tuning process, delivering consistent and reproducible results.
We evaluate the effectiveness of our approach by comparing the consistency (variance) and time required for alignment between the automated pipeline and three human engineers. The results show that the automated pipeline significantly outperforms manual alignment in both aspects. Specifically, the automated process reduces parameter variance by more than 2.5 times, demonstrating greater consistency and repeatability. Additionally, it completes the optimization in roughly one-third of the time required for manual tuning. The benefits of automation are particularly evident in scenarios involving interdependent variables, where manual attempts exhibit increased variance and require twice as much time.
Ultimately, both the quality and execution time of alignment are tied to the representativeness of simulated data. Consequently, further advancements in automation will likely involve the development of better virtual drivers to improve realism and optimize the tuning process further.

Anomaly Detection using LSTM-AE in Federated Learning Scenario

Rakesh Shrestha¹ Mohammadreza Mohammadi¹ Sima Sinaei¹ Alberto Salcines² David Pampliega³ Raul Clemente³ Ana Lourdes Sanz³

¹RISE ²TST ³Schneider Electric

In smart electric grid system, various sensors, and Internet of Things (IoT) devices are used to collect the electrical data at the substations. However, data collection might impose severe data misuse, data manipulation, or privacy leakage. In this poster, we presented anomaly detection technique using distributed Federated Learning (FL) framework to identify anomalies in industrial data that are gathered from the remote terminal devices deployed at the substations in the smart electric grid system.
Our proposed anomaly detection system is based on Long Short-Term Memory (LSTM) and Autoencoders (AE) and employs Mean Standard Deviation (MSD) and Median Absolute Deviation (MAD) approaches for detecting anomalies. FL preserves the privacy of the electrical data by enabling the energy providers to cooperatively train the shared AI model without disclosing the data to the server. Homomorphic encryption protects sensitive data while enabling numerous parties to contribute their data for model training by allowing calculations on encrypted data without the need for decryption. By maintaining secrecy, this cryptographic method improves the security of federated learning and fosters cooperative data analysis.
Currently, I am involved in an AI based quality assessment management project where we use advanced computer vision and zero shot learning to detect any defects on the industrial products as anomalies. We are working on generalized detection algorithm where the system can detect any class of defects on any type of industrial products, that means we donot have to train the model for each new defect type. I am also working on unmanned aerial vehicles utilizing federated learning techniques to preserve the privacy of the data collected by the UAV sensors and then integrate human in the loop (HITL) for providing decision knowledge when the autonomous UAV system can not give decisions on dynamic or unseen aerial environments.

Proving Safety at Sea

Simulation-Based Compliance Testing for Autonomous Ships

Sreekant Sreedhara¹, Erik Røsæg², Børge Rokseth^1
1Department of Engineering Cybernetics, NTNU. ²Faculty of Law, University of Oslo.

Autonomous vessels represent a significant advancement in maritime transportation, offering benefits such as reduced operational costs, improved safety, and lower environmental impact. However, ensuring their safe navigation and compliance with maritime regulations, particularly the International Regulations for Preventing Collisions at Sea (COLREGs), remains a major challenge. This research presents a novel safety assurance framework that employs a digital twin-based simulation environment for rigorous testing and validation of autonomous navigation systems. The proposed system integrates sensor and actuator models within a virtual testbed, enabling the dynamic generation and assessment of complex navigational scenarios. By leveraging automated test management, the framework identifies potential safety deficiencies, ensuring compliance with regulatory requirements.
Our approach combines large-scale probabilistic simulations with a structured rule-based evaluation mechanism to bridge the gap between AI-driven vessel behavior and human-explainable regulatory adherence. The framework introduces Legata, a specialized domain-specific language designed to codify maritime regulations in a machine-readable format. Additionally, the simulation platform, built on the Co-Simulation Operating System (COS), enables scalable and realistic scenario generation, ensuring comprehensive validation of collision avoidance and decision-making. The framework employs a containerized high-performance computing infrastructure to execute thousands of simulations in parallel, covering a vast array of navigational situations, environmental variables, and human interactions. By systematically evaluating vessel behavior in a controlled environment, the methodology provides a robust and scalable alternative to traditional verification approaches, which often rely on costly physical trials or incomplete test cases.