2018 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 |
2018年度は，以下の２つ成果を獲得した．
1.知能化システムを対象とした系統的評価法の提案．
機械学習を用いて実現された分類器に焦点を当て，その安全性を系統的に評価する手法を提案した．提案手法は，データセットに基づいた安全分析とテスト結果の統計的評価方法から構成される．安全分析では，よく知られているFTA(Fault Tree Analysis)をデータセットの取り扱いができるように拡張した．テストでは，この水準を満たしているか統計的に評価を実施する．提案手法は，CNN(Convolutional Neural Network)による手書き文字の分類器に適用し，評価を行った．
2. 大規模複雑MATLAB/Simulinkモデルのテンプレートに基づいたテスト手法の提案．
MATLAB/Simulinkモデルにおいてカバレッジ基準を満たすテストスイートを自動生成する手法を提案した．テストスイートを発見する標準的な手法は，条件分岐の制約充足を解析して，特定のパスを通る入力を発見するものである．しかしながら，MATLAB/Simulinkモデルでは，非線形算術計算のような複雑な演算を使用できるため，一般には，自動的に制約充足を判定できない．そこで，Monte-Carlo法を用いてMATLAB/Simulinkモデルの探索を行い，カバレッジ基準を満たすテストスイートを発見することにした．一方，MATLAB/Simulinkモデルでは，時系列データを入力とした動作を記述しているため，時間に伴う入力の変化を取り扱う必要がある．そこで，入力の時系列データの変化パターンを一般化したテンプレートを用いて乱択を行うことにした．そして，実用規模の大規模複雑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
2018年度は，以下の３つを実施する予定であったが，それらをおおむね予定どおり実施できた．
1. 知能化システムを対象とした検証実験の実施．知能化システムは不確定性を持つため，その検証に関しては未知なことが多い．そこで，2018年度は，手書き文字データセットMNISTを用いて手書き文字の識別器を構成し，その妥当性評価用データセットを獲得する手法の検討を行った．この実験により，検証用データセットの分類が重要であることが判明し，FTAを用いて検証用データセットを分析する手法，および，検証用データセットを用いて識別器のテストをする手法の提案に至った．
2. 大規模・複雑ハイブリッドシステムを対象としたシミュレーションによる検証
実験の実施．研究では，MATLAB/Simulinkで開発される大規模で複雑なシステムを対象とし，従来から研究されている記号実行などの静的な形式検証とモンテカルロ法などのシミュレーション手法を組み合わせて，規模と複雑さ の問題を解決する方法を明らかにする．2018年度は，まず，シミュレーション手法による検証実験を行った．この実験により，入力となる時系列データの典型的な形にのみ注目してモンテカルロ法を実施することにより，効果的にテストが実施できることが判明し，テンプレートに基づいたテスト手法の提案に至った．
3. メニーコアシステム向け基本ソフトウェアを対象とした検証実験の実施．2018年度は，車載システム関連会社と協力して商用のメニーコアオペレーティングシステム（OS）のテスト実験を行った．メニーコアOSでは，タスクの数や配置など，様々なコンフィギュレーションを考慮しなければならないため，テストの数が爆発的に多くなる．そこで，コンピュータクラスタを用いてテストを実施する環境を整えることができた．
|
| Strategy for Future Research Activity |
1.知能化システム(不確定性の取り扱いの明確化)．これまでに，手書き文字データセットMNISTを用いた検証実験とテスト手法の提案を行ったが，対象としている識別器とデータは単純なものである．今後は，物体認識や動画などの複雑なデータを取り扱う知能化システムを対象とする予定である．また，これまでは，機械学習，特に，識別器に焦点を当てた．今後は，回帰学習器などの手法についても考慮していく予定である．
2.ハイブリッドシステム(大規模・複雑演算の取り扱いの明確化)．これまでに，テンプレートとモンテカルロ法を用いたテストスイート生成手法を提案した．しかしながら，モンテカルロ法のみでは，カバレッジ基準を満たすことが難しいパスも存在する．そこで，今後は，MATLAB/Simulinkモデルで用いられている計算や構造の分析を併用し，より効果的にテストスイートを生成する手法について検討していく予定である．
3.メニーコアシステムと成果の統合(高度スケジューリング，不確定性・大規模・複雑演算の抽象化の明確化)．これまでに，コンピュータクラスタを用いてテストを実施する環境を整えた．この環境では，メニーコアOSにおいて期待する振る舞いのモデルを仕様記述言語PROMELAを用いて記述する．PROMELAはモデル検査ツールSPINのための仕様記述言語であり，SPINを用いてモデル検査を実施することができる．本研究では，SPINを用いてモデルを探索し，網羅的なテストケースを生成する手法を，すでに提案している．そこで，この手法を用いてメニーコアOSのテストを実施し，その際の問題点を明らかにしていく予定である．
|
