| 研究課題/領域番号 |
18H03220
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
青木 利晃 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (20313702)
|
|---|
| 研究分担者 |
石井 大輔 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2023-03-31
|
| キーワード | 形式手法 / 車載システム / ハイブリッドシステム / テスト |
|---|
| 研究実績の概要 |
2021年度は以下の３つの成果を獲得した．
1. 自動運転システムを対象とした形式仕様ベーステストを提案した．本研究では，これまでに，形式仕様記述言語BBSL(Bounding Box Specification Language)を提案した．2021年度は，BBSLで記述された仕様(BBSL仕様と呼ぶ)に基づくテスト手法を提案した．BBSL仕様には，画像などの入力に対して，知能化システムがどのような出力をすべきか記述する．提案手法では，BBSL仕様に記述されている出力をテストの期待値とみなす．そして，画像(入力)を知能化システムに与えた時の出力と，BBSL仕様で規定されている期待値を比較してテストを実施する．
2. SMTソルバを利用した大規模複雑MATLAB/Simulinkモデルの検証手法を提案した．大規模複雑MATLAB/Simulinkモデルを検証するためにはスケーラビリティに関する問題の解決が必要である．そこで，2021年度は，assume-guarantee手法を用いた分割検証手法を提案した．これにより，MATLAB/SimulinkモデルをSMTソルバで取り扱うことができる規模に分割し，それらを統合して検証することが可能になった．
3. メニーコアOSを対象とする不確定性を考慮したテスト手法を提案した．本研究では，モデル検査ツールSPINを用いたメニーコアOSの検証手法を提案してきた．その後，SPINでは柔軟な状態探索が困難であることが判明した．そこで，2021年度は，汎用プログラミング言語Rustを用いたテストケース自動生成手法を提案した．提案手法では，状態探索中に，複数の動作の可能性がある部分(すなわち，不確定性を持つ部分)を特定し，非決定的な遷移を含む探索木を作成する．そして，探索木を走査して，非決定的な遷移を含む遷移列をテストケースとして自動生成する．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
2021年度は以下の３つを実施する予定であったが，以下のとおり，それぞれ，おおむね予定どおり実施できた．
1. 自動運転システムを対象とした形式仕様ベーステスト手法の提案．研究実績に示したとおり，2021年度中に自動運転システムを対象とした形式仕様ベーステストを提案することができた．現在は，提案手法に基づいて，公開データセットの１つであるWaymo Open Datasetを用いて実験を実施している．手法の提案および実験を実施できていることから，本研究項目は，おおむね予定どおり実施できていると考えている．
2. SMTソルバを利用した大規模複雑MATLAB/Simulinkモデルの検証手法の提案．研究実績に示したとおり，2021年度中にSMTソルバを利用した大規模複雑MATLAB/Simulinkモデルの検証手法を提案することができた．比較的小規模であるが実践的な状況を含むMATLAB/Simulinkモデル，および，大規模複雑なMATLAB/Simulinkモデルに提案手法が適用できることを確認した．よって，本研究項目は，おおむね予定どおり実施できていると考えている．
3.メニーコアOSを対象とする不確定性を考慮したテスト手法の提案．研究実績に示したとおり，2021年度中に，メニーコアOSを対象とする不確定性を考慮したテスト手法を提案することができた．現在，メニーコアOSの例としてPOSIXに準拠したLinuxを対象に提案手法の適用実験を実施している．手法の提案および実験を実施できていることから，本研究項目は，おおむね予定どおり実施できていると考えている．
|
| 今後の研究の推進方策 |
2022年度は，本研究課題の最終年度となる．そこで，これまでの成果を統合し，次世代車載システムのための形式手法としてまとめる．提案手法は，知能化システムのための手法，ハイブリッドシステムのための手法，メニーコアシステムのための手法により構成される．
1. 知能化システムのための手法の提案．2022年度は，他手法と統合するため，ハイブリッドシステムの動作を考慮したBBSL仕様を作成し，これまで提案してきた仕様ベーステスト手法を適用する実験を実施する．実験では，Waymo Open Datasetなどの公開データセットを用いる．一方，テストでは，それらの画像が，様々な状況をカバーしていることが重要である．そこで，現在，カバーしている状況を表現する指標，すなわち，カバレッジ指標について検討を行う．そして，実験に基づいて，BBSLの利点と欠点を整理し，必要であればBBSL，および，仕様ベーステスト手法を拡張する．
2. ハイブリッドシステムのための手法の提案．本研究では，これまでに，乱択に基づいた手法を提案し，その後，SMTソルバに基づいた手法を提案してきた．2022年度は，これらの手法を併用する手法を提案する．また，知能化システムへの入出力を行うモデルを実験の題材とする．これにより，知能化システムのための手法との連携について検討し，必要であれば，これまで提案してきた手法を拡張する．
3. メニーコアシステムのための手法の提案．2022年度は，POSIX OSとGPUを組み合わせたシステムの検証実験を実施する．これにより，知能化システム，および，ハイブリッドシステムの実行を想定して，提案手法の有効性について評価することができる．実験に基づいて，提案手法の利点と欠点を整理し，必要であれば提案手法を拡張する．
|
