2022 Fiscal Year Final Research Report
Study on formal methods for next-generation automotive systems
| Project/Area Number |
18H03220
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
Aoki Toshiaki 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (20313702)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
石井 大輔 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | 形式手法 / 形式検証 / 形式仕様記述 / 車載システム / ハイブリッドシステム / モデル検査 / 充足可能性判定 / テスト |
|---|
| Outline of Final Research Achievements |
In this research, we proposed a formal method and a verification method for next-generation automotive systems to achieve their high reliability and high safety. The next-generation automotive systems face problems regarding uncertainty coming from intelligent systems, handling of a large amount of diverse data including images and videos, and computational complexity arising from advanced control. In this research, we proposed an extended and specialized version of conventional formal methods as well as new formal methods to solve and mitigate these problems. We also proposed solutions in combination with the other methods such as testing, modeling, and simulation to make our formal methods practical. We demonstrated the effectiveness of our method using open datasets and public documents. In addition, some of the research results have been successfully released as a commercial tool. Thus, we can say that we succeeded in proposing a practical method.
|
| Free Research Field |
ソフトウェア工学
|
| Academic Significance and Societal Importance of the Research Achievements |
形式手法は，一筋縄では実践が行えないため，実践のための理論や技術も学術的な研究の対象である．本研究では，形式手法を用いた複数の実践例を示すことができ，次世代車載システムのような先進システムにおいても形式手法が有効であることを示すことがでた．これは，当該分野の発展に大きく貢献すると考えている．また，本研究では，提案手法に基づいたツールを実装し，商用ツール，および，オープンソースとしてリリースした．これらは，産業界に直接的に還元できるものである．本研究の成果が普及することにより，自動車に限らず，同様の先進システムの信頼性・安全性が格段に高くなり，安全・安心な社会構築へ貢献することが期待される．
|
