Formal Methods and Verification Tools for Next-generation Automotive System Platforms
SCROLL
OUTLINE
In this research, we propose formal methods and verification tools to ensure the safety and reliability of next-generation automotive system platforms. The formal methods consist of a formal specification language, a control specification language, and formal verification methods using these languages. We propose the verification tools to support them as well. Such formal methods and verification tools cover the recognition to control functions of the next-generation automotive system platforms, and we stick in their practical application to real systems. The results of this research are expected to drastically improve the safety and reliability of automotive systems, and that will contribute to realizing our safe and reliable mobility society with next-generation cars including autonomous cars.
Research Goals
Our research goals are to propose practical formal methods and verification tools for next-generation automotive system platforms as well as to quantitatively show their effectiveness based on open data and autonomous driving experiments.
Related Work and Challenges
Many autonomous driving demonstration experiments are being conducted. Most of them are to study control theories and mobility services. There are also many studies to apply formal methods and formal verification to automotive electronic control systems; however, most of them simplified target systems or focused on a small part of them. Our formal methods and verification tools proposed in this research cover the perception to control functions of the automotive system platforms, which are more practical and realistic than the existing works. The advantage of this research is that we stick in applying scientific approach, that is, formal methods, to real automotive system platforms. To the best of our knowledge, there have been no reports that the safety and reliability of autonomous driving systems are comprehensively verified by formal methods. The results of this research is expected to be the first such case.
Future Deployment ＆ Research Plan
We plan to promote the proposed formal methods and tools to industry after the research period. We will provide the tools proposed in this research as commercial or open source tools so that they can be immediately used in industrial projects. In addition, we will make data obtained by open data and collaboration with automated driving demonstration experiments public. Such data show the effectiveness of our formal methods and will attract industry. Based on such tools and data, we try to apply our formal methods to actual automotive system platforms used in actual car products with automotive companies. These series of activities planned after the research period are expected to drastically improve the safety and reliability of the next generation of cars.