2020 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 |
2020年度は以下の３つの成果を獲得した．
1.形式仕様記述言語BBSLの定理証明システムCoqによる形式化．2019年度に提案した形式仕様記述言語BBSLの理論を定理証明システムCoq上に実現した．まず，BBSLの抽象構文をCoqの型で表現した．BBSLは区間計算に基づいて定義されているため，Coq上に区間に関する理論を構築し，BBSLの意味論を定義した．これは，いわゆる，deep dmbeddingと呼ばれる方法である．これにより，BBSLで記述した形式仕様をCoqで検証することが可能になった．
2.MATLAB/SimulinkモデルからSMT-LIB形式に変換するツールのプロトタイプ実装．MATLAB/Simulinkモデルから，SMTソルバのための標準的な記法であるSMT-LIB形式に変換するツールのプロトタイプを作成した．これにより，自動的に，MATLAB/SimulinkモデルからSMT-LIB形式に変換し，SMTソルバにより充足可能性判定することができ，大規模な実験を行うことが可能になった．また，大規模MATLAB/Simulinkモデルの検証実験を行ったところ，分割検証が必須であることが判明した．
3.商用メニーコアOSの実践的検証の実施．本研究では，これまでに，モデル検査ツールSPINを用いて網羅的なテストケース，および，テストプログラムを自動生成し，メニーコアOSの大規模テストを実施する手法について検討を行ってきた．そこで，車載システム向けの商用OSを対象にして，大規模な検証を実施した．本検証では，NICTのStarBEDを利用した．その結果，妥当な時間での網羅的なテストに成功し，これまでに，17個の誤りを発見することができた．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
2020年度は以下の３つを実施する予定であったが，以下のとおり，おおむね予定どおり実施できた．
1. 自動運転システムを対象とした検証実験の実施．2020年度は，画像認識システムYOLOの検証実験を行った．自動車の追従など特定のシナリオに焦点を当て，自動運転シミュレータCARLAを用いて画像を生成した．また，西日などの要因をCARLAで再現し，YOLOが正しく認識できるか検証した．その結果，障害を伴う状況では，大きく認識率がおちることを確認できた．これは，YOLOが，自動運転に特化して学習を行っていないことに起因するものと考えられる．
2. 記号実行およびSMTソルバを併用した大規模複雑MATLAB/Simulinkモデルの検証実験の実施．大規模複雑MATLAB/Simulinkモデルを手作業でSMTソルバで取り扱い可能な形式に変換するのは現実的でない．そこで，まず，MATLAB/SimulinkモデルからSMT-LIB形式に変換するツールのプロトタイプ実装した．そして，このツールを用いて，大規模複雑MATLAB/Simulinkモデルの検証実験を行うことができた．
3.メニーコアOSを対象とする不確定性を考慮したテスト実験の実施．メニーコアOSでは，コア間のマイグレーションを伴い，かつ，柔軟なスケジューリングが行われるため，実行に関する不確定性が存在する．そこで，POSIX OSを対象にテスト実験を実施した．スレッドの起動とマイグレーションに焦点を当て，結果が不確定となる場合について分析した．これにより，網羅的なテストケースを生成する際の状態探索アルゴリズムに拡張が必要なことが判明した．そこで，2021年度は，状態探索アルゴリズムを柔軟に変更しながら，テストケースを生成する手法について検討を行う予定である．
|
| Strategy for Future Research Activity |
今後の研究の推進方策は以下のとおりである．
1.知能化システム．研究を開始した当初は，手書き文字データセットMNISTを用いていたが，その識別器とデータは単純なものであった．そこで，2020年度は，自動運転シミュレータCARLAを用いて，より複雑で現実的な画像を生成した．しかしながら，運転コースの形状などを指定する必要があり，柔軟な画像の生成は困難であった．一方，現在，自動車メーカーやIT企業により，自動運転のデータセットが公開されている．今後は，これらのデータセットを積極的に活用しようと考えている．
2.ハイブリッドシステム．2020年度はSMTソルバを用いてMATLAB/Simulinkモデルを検証する手法について検討を行った．ここでは，MATLAB/Simulinkモデルが大規模である場合，SMTソルバの充足可能性判定が終了しないという問題があった．MATLAB/Simulinkモデルのエンコード形式を最適化するだけでは，この問題の解決は不可能であると考えている．そこで，assume-guaranteeによる分割検証について検討を行うことにした．
3.メニーコアシステム．これまでに，期待する振る舞いのモデルを仕様記述言語PROMELAを用いて記述し，その正しさをモデル検査ツールSPINで検証し，網羅的なテストケースおよびテストプログラムを生成する手法を提案した．現在は，POSIX OSのように柔軟なスケジューリングを行うOSを対象として，同様のアプローチによる手法の提案を検討している．2020年度に実施したテスト実験により，状態探索アルゴリズムの拡張が必要なことが判明した．これまで通りSPINを用いると状態探索アルゴリズムの変更が困難である．そこで，まずは，C言語などの汎用プログラミング言語でテストケースの自動生成を行おうと考えている．
|
