Verifying Autoware Controller Node by Combining Model Verification and Runtime Monitoring

Daisuke Ishii

Home/Archive/arXiv

arXiv · 2610.15418

Verifying Autoware Controller Node by Combining Model Verification and Runtime Monitoring

Daisuke Ishii

View original source ↗Read source document ↗Export metadata ↓

Abstract

Formal modeling and verification of autonomous driving systems remain challenging due to the vast operational space and the complexity of the control logic. We propose a hybrid verification approach that combines formal model verification and runtime monitoring for the trajectory-following control node of Autoware, an open-source autonomous driving platform. We formalize the controller as a hybrid system in differential dynamic logic (dL), and introduce an abstract model that captures the essential control dynamics. We then prove safety and liveness properties of the model using the KeYmaera X proof assistant. Complementarily, we monitor the constraints that assure the compatibility between the model and the Autoware implementation across numerical simulation runs using the Autoware toolchain, quantifying to what extent the implementation's behavior is subsumed by the verified model. The experimental results confirmed that (i) monitoring provides a sound evaluation of target following with accuracy bounds, and (ii) the Autoware implementation reaches the target with an accuracy of approximately 0.2-0.4 (m) in position and 0.8 (m/s) in velocity.

Explore related subjects

cs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Daisuke Ishii. 2026-10-11. Verifying Autoware Controller Node by Combining Model Verification and Runtime Monitoring. https://arxiv.org/abs/2610.15418

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Towards a Taxonomy of Software Log Smells

Logging is an important part of modern software projects; logs are used in several tasks such as debugging and testing. Due to the complex nature of logging, it remains a difficult task with several pitfalls that could have serious consequences. Several other domains of software engineering have mitigated such threats by identifying the early signs of more serious issues, i.e., ``smells''. However, in the context of software logging, the concept of smells has only been investigated in a limited and narrow scope. The goal of this study is to systematically organize logging issues reported in the literature into a taxonomy of log smells that can help practitioners to better understand logging quality issues. To further help the practitioners and to identify issues that need more attention from the research community, we also map the identified smells to existing tools repairing them. We conducted a survey of the scientific literature to identify logging issues and related tools. After extracting relevant data from 61 articles, we used open coding to define logging issues and applied card sorting to derive log smells from these issues. Finally, we classified the tools based on their reported output. We present a taxonomy of nine log smells, describe several facets for each of them, and report the results of a preliminary validation of the taxonomy using a dataset of logging issues extracted from open-source projects. We also review existing tools repairing/removing some of these facets, highlighting the lack of tools addressing some log smells and identifying future research opportunities to close this gap. Our findings indicate that software logging is susceptible to a wide variety of log smells affecting both the logging code and the resulting log files. Understanding these smells, along with their causes and consequences, can help reduce their occurrence and improve logging quality.

cs.SE↗

arXiv2026

From Empirical Evaluation to Context-Aware Enhancement: Repairing Regression Errors with LLMs

[...] Since then, various APR approaches, especially those leveraging the power of large language models (LLMs), have been rapidly developed to fix general software bugs. Unfortunately, the effectiveness of these advanced techniques in the context of regression bugs remains largely unexplored. This gap motivates the need for an empirical study evaluating the effectiveness of modern APR techniques in fixing real-world regression bugs. In this work, we conduct an empirical study of APR techniques on regression bugs. To facilitate our study, we introduce RegressionBug4APR, a high-quality benchmark of Java and Python regression bugs integrated into a framework designed to facilitate APR research. The current benchmark includes 200 regression bugs collected from widely used real-world GitHub repositories. We begin by conducting an in-depth analysis of the benchmark, demonstrating its diversity and quality. Building on this foundation, we empirically evaluate the capabilities of APR to regression bugs by assessing both traditional APR tools and advanced LLM-based APR approaches. Our experimental results show that classical APR tools fail to repair any bugs, while LLM-based APR approaches exhibit promising potential. Motivated by these results, we investigate impact of incorporating bug-inducing change information into LLM-based APR approaches for fixing regression bugs. We further conduct an ablation study to disaggregate the contribution of each contextual element within the bug-inducing change information. Our results highlight that this context-aware enhancement significantly improves the performance of LLM-based APR, yielding 1.6x more successful repairs compared to using LLM-based APR without such context. Moreover, our findings are consistent across both Java and Python benchmarks, providing preliminary evidence for the generalizability of our findings.

cs.SE↗

arXiv2026

Parameter-Efficient Multi-Task Fine-Tuning in Code-Related Tasks

Large Language Models (LLMs) have proven highly effective in automating software engineering tasks, bridging natural language and code semantics to achieve notable results in code generation and summarization. However, their scale incurs substantial computational costs, making full fine-tuning impractical. Parameter-Efficient Fine-Tuning (PEFT) methods like QLoRA enable efficient specialization with lower resource demands. Recent studies show QLoRA-optimized Large Code Models (LCMs) perform strongly across diverse tasks, yet it remains unclear whether this effectiveness persists when a single model is QLoRA fine-tuned for multiple code-related tasks. The interaction between Multi-task fine-tuning and QLoRA optimization, and how transfer learning affects correctness and quality of generated artifacts, remains largely unexplored. We investigate Multi-task QLoRA fine-tuning --- a representative parameter-efficient method from the LoRA family --- across three representative tasks: code generation, translation, and summarization. We evaluate functional correctness through execution-based and similarity-based metrics, complemented by comprehensive code quality analysis--an aspect largely overlooked in prior work. Our findings show that Multi-task QLoRA effectively leverages transfer learning, achieving competitive or superior performance at the 1.5B, 3B, and 7B configurations relative to both Single-task QLoRA and Multi-task full fine-tuning. Larger models demonstrate more consistent balance between correctness and quality, whereas smaller models preserve functionality but exhibit a higher incidence of quality-related issues.

cs.SE↗