2019 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 |
2019年度は，以下の３つの成果を獲得した．
1.自動運転システムを対象とした画像に関する仕様記述手法の提案．自動運転システムでは，画像や軌道などの複雑なデータが対象であるが，それらを明確に表現する仕様記述法は確立していない．幾何学的に表現することも考えられるが，試行錯誤を行いにくく，仕様記述に適していない．画像認識では，Bounding Boxがよく用いられるが，仕様記述の観点からは，Bounding Boxは画像の抽象化と捉えることもできる．そこで，区間を用いて，画像上の位置関係の仕様を厳密に記述する形式仕様記述言語BBSLを提案した．
2.自動運転システムを対象としたテストシナリオのモデル化手法の提案．自動運転におけるテストシナリオは，自然言語や位置関係を表現する補助的な絵を用いて記述される場合が多い．テストシナリオでは，複数の自動車が特定の軌道で移動する場合を規定しているが，それらを明確に記述する標準的な手法が存在しないのが現状である．そこで，UMLのアクティビティ図を参考に，自動車の位置関係とそれらの動作を記述可能な道路位置関係図を提案した．
3.大規模複雑MATLAB/Simulinkモデルの定数伝搬に基づいたテスト手法の提案．2018年度までに，MATLAB/Simulinkモデルのシミュレーションによるテスト実験を実施し，単純なMonte Carlo法でも，ある程度の範囲をカバーできることが確認できた．しかしながら，すべてのブロックを網羅するためには，モデルの内部的な構造を解析する必要があることが判明した．MATLAB/Simulinkモデルには，非線形演算などの複雑な演算が含まれているため，直接的な解析は困難である．そこで，モデル中の定数に注目し，その伝搬を解析しテストする手法を提案した．これにより，テストの効率を大幅に向上させることができた．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
2019年度は以下の３つを実施する予定であったが，それらをおおむね予定どおり実施できた．
1. 知能化システムを対象とした，より複雑な検証実験．米国のNational Highway Traffic Safety Administration(NHTSA)により取りまとめられた，自動運転システムのためのテストに関する文書に着目し，その中で規定されているテストシナリオを形式的に取り扱う手法について検討を行った．これにより，画像上の位置関係の仕様を厳密に記述する形式仕様記述言語BBSLおよび自動車の位置関係とそれらの動作を記述可能な道路位置関係図を提案した．さらに，NHTSAの文書の一部を提案手法で記述し，有効性を確認することができた．
2. 大規模・複雑ハイブリッドシステムを対象とした効率的な検証手法の模索．2018年度までに提案したテスト手法ではカバーすることが困難であったブロックを取り扱う手法について検討を行った．そして，モデル中に出現する定数の伝搬を解析し，効果的にMonte Carlo法を実施することができた．これにより，現実的な規模と複雑さを持つモデルに対して，ブロックのカバー率が向上することを確認できた．
3. メニーコアシステム向け基本ソフトウェアを対象としたモデルベーステスト実験の実施．2019年度は，Classic AUTOSARとAdaptive AUTOSARに基づいたマルチコアOSのモデルを作成し，そのモデルに基づいたMBT(Model Based Testing)を実施することができた．期待する振る舞いのモデルを仕様記述言語PROMELAを用いて記述し，モデル検査ツールSPINを用いて網羅的なテストケースを生成することができた．さらに，生成したテストケースからテストプログラムを自動生成し，コンピュータクラスタ上でテストを実施することができた．
|
| Strategy for Future Research Activity |
今後の研究の推進方策は以下のとおりである．
1.知能化システム(不確定性の取り扱いの明確化)．これまでに，手書き文字データセットMNISTを用いた検証実験とテスト手法の提案を行ったが，対象としている識別器とデータは単純なものであった．2019年度は，自動運転システムにおける画像を対象とした仕様記述およびテストシナリオ記述法を提案した．そこで，今後は，自動運転システムで用いられるような画像を用いて，機械学習システムを検証する実験を実施する予定である．
2.ハイブリッドシステム(大規模・複雑演算の取り扱いの明確化)．これまでに，テンプレート，および，定数伝搬を用いてモンテカルロ法によりテストスイートを生成する手法を提案した．これにより，MATLAB/Simulinkモデルに出現するブロックの大半をカバーすることに成功した．しかしながら，まだ，カバーできていないブロックが存在する．そこで，記号実行およびSMTソルバを併用する手法について検討する予定である．
3.メニーコアシステムと成果の統合(高度スケジューリング，不確定性・大規模・複雑演算の抽象化の明確化)．
これまでに，メニーコアOSにおいて期待する振る舞いのモデルを仕様記述言語PROMELAを用いて記述し，その正しさをモデル検査ツールSPINで検証し，網羅的なテストケースおよびテストプログラムを生成することに成功した．実際にテストを実施すると，テストプログラムで期待したとおりに実行されない場合が多く存在することが判明した．メニーコアOSでは，コア間のマイグレーションを伴い，かつ，柔軟なスケジューリングが行われるため，実行に関する不確定性が存在するのである．そこで，このような不確定性を扱う方式について検討を行う予定である．
|
