2022 Fiscal Year Research-status Report
Constraint Acquisition and Compositional Verification of Large and Complex Cyber-Physical Systems
| Project/Area Number |
22K11969
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
石井 大輔 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
|
|---|
| Project Period (FY) |
2022-04-01 – 2026-03-31
|
| Keywords | サイバーフィジカルシステム / 制約プログラミング / 制約獲得 / 部品化検証 |
|---|
| Outline of Annual Research Achievements |
大規模複雑なサイバーフィジカルシステム（CPS）の制約獲得や部品化検証を可能にすることを目標に，3研究項目を実施した．
（1）MATLAB/Simulinkモデルの網羅テスト手法について研究した．CPSモデリングツールであるSimulinkで記述したモデルに対し，入力信号を探索し，モデル中のテスト項目の達成網羅率を向上するための手法を設計・実装した．提案手法は，述語論理式ソルバーに基づく既存手法に基づくが，本研究項目では，部品化検証アプローチによりテスト生成処理の効率化に取り組んだ．Simulinkモデルのサブシステム構造を利用し，浅い階層だけを探索したり，一部を抽象化したりする処理を検討した．提案手法をMATLAB上に実装し，大規模複雑な例を用いて実験的に評価した．その結果，提案手法が正しく動作することと，既存ツールと比較して良好な性能が得られることがわかった．
（2）ロボットアームの適合度テスト手法について研究した．ROSフレームワークを用いたロボットのモデルベース開発では，ロボットのモデルと実機の適合度が重要である．本研究項目では，ROSのモーションプランニング部品の出力と，実ロボットの動作結果との適合性の判定方法を検討し，複数の判定結果からモデルと実機の適合度を定量評価する方法を設計・実装した．提案手法は，ROSの機構を利用して軌道データを取得し，時間・空間方向の摂動を許容しながら適合性を評価する点を特徴とする．Niryo Nedロボットについて提案手法によるケーススタディを実施するとともに，提案手法の実例に対する有効性を確認した．
（3）機械学習による運転者の状態推定手法について研究した．運転者支援系への利用を想定し，状態推定手法について調査・実験を行った．運転シミュレーターと脳波計を用い，眠気判定を示すデータを同定し，操舵の癖を機械学習する方法について検討した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究実施計画に従い研究を進め，一定の成果を得ることができた．研究項目（1）では，大規模複雑CPSの検証の一形態として，Simulinkで記述したモデルのテストについて研究した．サブシステム（部品）を利用したモデルの抽象化や効率的なテスト生成処理の手法を検討した．提案手法を実装し，収集した大規模複雑なモデル例に対して適用する実験を実施した．研究項目（2）では，機械学習（ML）を用いないCPSの例として，ロボットアームの適合性検査に取り組んだ．研究項目（3）では，MLを用いるCPSの例として運転者支援系の調査・実験に取り組んだ．前記の結果は，研究実施計画の複数項目に対応するものと考えている．現状，制約獲得の事前準備として，既存のモデル・制約記述の仕組みに依拠して研究している．また，ML部品と非ML部品が混在するCPSに対する手法開発にはまだ取り組んでいない．
|
| Strategy for Future Research Activity |
制約獲得と部品化検証の手法を明らかにし，大規模複雑CPSの検証を可能にするため，以下の研究項目に取り組む．
【A．大規模複雑CPSの検証】より積極的に部品を利用した検証手法の開発に取り組む．契約が付与された部品からなるモデルの効率的な検証手法や，モデルの自動部品化，契約の自動付与などの機能を検討する．ML部品と非ML部品からなるCPSを扱う方法を検討する．また，CPSの制約・モデル・実機について適合性を検査する方法を検討する．
【B．非ML部品の要約，契約の獲得】ロボットアーム等を題材として，詳細なモデルを記述する実験を行う．同時に，対象のモデル記述や制約を自動獲得する方法を検討する．また，モデルの部品化と，部品間の契約の獲得方法を検討する．
【C．ML部品の検証】ロボットアームや自動運転系を題材として，ML部品の仕様・モデル・契約を記述し，訓練データセットや他の部品との整合性を検査する実験を行う．また，記述作業やデータの整備作業を支援したり，自動化したりする手法を検討する．
|
| Causes of Carryover |
コロナ禍により当初予定していた旅行を実施しなかったため．翌年度以降の成果発表や旅行にて使用する予定である．
|
Research Products
(3 results)
