2022 Fiscal Year Annual Research Report
Study on formal methods for next-generation automotive systems
| Project/Area Number |
18H03220
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
青木 利晃 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (20313702)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
石井 大輔 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | 形式手法 / 車載システム / ハイブリッドシステム / テスト |
|---|
| Outline of Annual Research Achievements |
2022年度は，本研究課題の最終年度となる．そこで，これまでの成果を統合し，次世代車載システムのための形式手法としてまとめると共に，評価のための実験を実施した．提案手法は，知能化システムのための手法，ハイブリッドシステムのための手法，メニーコアシステムのための手法により構成される．
1. 知能化システムのための手法．本研究では，これまでに，形式仕様記述言語BBSL(Bounding Box Specification Language)，および，BBSLで記述された仕様(BBSL仕様と呼ぶ)に基づくテスト手法を提案した．今年度は，Yolov3を自動運転システムの画像認識部分に利用することを想定した実験を実施した．実験では，いくらかの非安全な誤認識が発生することを検出することができた．これにより，提案手法が，実践的な自動運転システムにおいて有効に働くことを確認できた．
2. ハイブリッドシステムのための手法．本研究では，これまでに，乱択に基づいた手法を提案し，その後，SMTソルバに基づいた手法を提案してきた．2022年度は，これらを併用する手法を提案した．また，実践的なMATLAB/Simulinkモデルを用いた実験を実施し，個々の手法，および，競合ツールであるSLDV(Simulink Design Verifier)に勝ることを確認することができた．
3. メニーコアシステムのための手法．本研究では，これまでに，汎用プログラミング言語Rustを用いたメニーコアOSのテストケース自動生成手法を提案した．本年度は，POSIX準拠のLinuxを対象とした実験を実施し，提案手法の評価を行った．これにより，メニーコアOSの仕様と実装の間に多くの乖離があることが検出でき，提案手法の有効性を確認できた．
|
| Research Progress Status |
令和4年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和4年度が最終年度であるため、記入しない。
|
