We are working on the practical application of formal methods to automotive systems. So far, we have conducted joint research with more than ten companies in the automotive domain. Our research has consistently focused on applying formal methods to real industrial products.

Our first major project focused on automotive operating systems compliant with the OSEK/VDX standard, which later evolved into AUTOSAR OS. In this project, we conducted practical verification by combining model checking and formal specifications with software engineering techniques such as testing. This collaboration continued for more than ten years, during which we verified two commercial operating systems. Following this, we received many joint research offers from suppliers and achieved several practical outcomes. We applied formal methods to support ISO 26262 compliance for a commercial electric power steering system. We also developed verification techniques for microcontrollerbased systems and applied them to MCAL (Microcontroller Abstraction Layer) modules. Furthermore, we proposed methods to support coverage requirements in model-based development using MATLAB/Simulink, leading to the development and release of the commercial tool PROMPT.

Today, autonomous driving has become a global focus. Our previous work mainly targeted individual modules of automotive systems, namely in-vehicle systems. In contrast, autonomous driving systems are fundamentally different from these systems, as they generate control commands that are executed by invehicle systems. They integrate AI technologies with image processing, sensing, and control. However, since AI systems often behave as black boxes, methods for ensuring their reliability and safety are not yet fully established. In response to this shift, we have expanded our research focus to include autonomous driving systems. Recently, we launched a JST/CREST project titled “Formal Methods and Verification Tools for Next-generation Automotive System Platforms.” This project aims to develop formal methods and verification tools to ensure the safety and reliability of autonomous driving systems. As in our previous work, we continue to emphasize applying formal methods to real systems, currently using Autoware as our target platform.

In this talk, I will first present the research results we have achieved so far, as well as the practical lessons learned from our industrial collaborations, and then introduce an overview of the JST/CREST project.