Constraint Acquisition and Compositional Verification of Large and Complex Cyber-Physical Systems

点击翻译按钮获取中文摘要

大規模複雑なサイバーフィジカルシステム（CPS）の制約獲得や部品化検証を可能にすることを目標に，3研究項目を実施した．（1）MATLAB/Simulinkモデルの網羅テスト手法について研究した．CPSモデリングツールであるSimulinkで記述したモデルに対し，入力信号を探索し，モデル中のテスト項目の達成網羅率を向上するための手法を設計・実装した．提案手法は，述語論理式ソルバーに基づく既存手法に基づくが，本研究項目では，部品化検証アプローチによりテスト生成処理の効率化に取り組んだ．Simulinkモデルのサブシステム構造を利用し，浅い階層だけを探索したり，一部を抽象化したりする処理を検討した．提案手法をMATLAB上に実装し，大規模複雑な例を用いて実験的に評価した．その結果，提案手法が正しく動作することと，既存ツールと比較して良好な性能が得られることがわかった．（2）ロボットアームの適合度テスト手法について研究した．ROSフレームワークを用いたロボットのモデルベース開発では，ロボットのモデルと実機の適合度が重要である．本研究項目では，ROSのモーションプランニング部品の出力と，実ロボットの動作結果との適合性の判定方法を検討し，複数の判定結果からモデルと実機の適合度を定量評価する方法を設計・実装した．提案手法は，ROSの機構を利用して軌道データを取得し，時間・空間方向の摂動を許容しながら適合性を評価する点を特徴とする．Niryo Nedロボットについて提案手法によるケーススタディを実施するとともに，提案手法の実例に対する有効性を確認した．（3）機械学習による運転者の状態推定手法について研究した．運転者支援系への利用を想定し，状態推定手法について調査・実験を行った．運転シミュレーターと脳波計を用い，眠気判定を示すデータを同定し，操舵の癖を機械学習する方法について検討した．