| 研究課題/領域番号 |
18K11240
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
石井 大輔 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2023-03-31
|
| キーワード | ハイブリッドシステム / 制約プログラミング / 区間解析 / 探索・論理・推論アルゴリズム |
|---|
| 研究実績の概要 |
連続・離散ハイブリッドシステムのための制約プログラミング技術を開発することを目標に，モデリングツールであるMATLAB/Simulinkのための検証およびテスト手法を検討した．今年度はおもに3項目を実施した．
（1）浮動小数点数（FP数）を変数とする制約充足問題に関し，元の制約式を実数を変数とする制約式に変換し，求解する手法について研究した．たとえばSimulinkモデルの検証において，FP数を用いた計算処理を高信頼に解析するのが重要である．FP数制約を扱うソルバーが提案されているが，実数制約のソルバーに較べ求解効率が悪いため，本項目では実数ソルバーを用いてFP数制約を求解する手法を検討した．提案手法はFP数を実数区間で保守的に近似する変換を施し，実数ソルバーにより近似的に求解をおこなう．提案手法が効果的であることを実験的に確かめた．とくに，丸め方向を変数とした問題をFP数ソルバーよりも効率よく解くことができた．
（2）複雑なSimulinkモデルを正確に制約式に変換する手法について研究した．これまで開発してきたSimulinkモデルの検査手法において，モデルを制約式（述語論理式）に変換する処理を拡張した．まず，これまで扱えなかった複合レートシステムや複合信号を扱う方法を検討した．つぎに，モデルが扱うFP数や整数をFP数やビット列で表す変換方法を検討した．変換方法をMATLAB上に実装し，正しく動作することを実験的に確かめた．
（3）モンテカルロ法と制約ソルバーを組み合わせたSimulinkモデルの網羅テスト手法について研究した．既存のモンテカルロ法による網羅テストとともに，制約ソルバーを用いた検査を実施し，テスト項目を達成・デッドロジック判定する手法を検討した．ツールを設計・実装し，複数のSimulinkモデルを用いた実験をした結果，既存ツールよりも高カバレッジを達成できた．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
今年度は，おもに研究項目A「大規模複雑なMATLAB/Simulinkモデルの解析が可能な制約プログラミング技術」と研究項目B「統計的手法（モンテカルロ法）の利用」を進めた．実例を用いた実験と成果発表に関して進捗がやや遅れている．前年度に計画した分割検証には取り組むことができなかった．研究実績（1）においては提案した求解手法の検証（研究項目C）もおこなった．研究項目Dについては今後研究実績（3）の並列化に取り組む予定である．
|
| 今後の研究の推進方策 |
計画の達成を目指し，ハイブリッドシステムのための制約プログラミング技術開発を進める．
（A）研究実績の3項目を組み合わせて大規模複雑なSimuilinkモデルを効率よく検証・テストするための手法の実現を目指す．また，Simulinkモデルを部品に分割して検証・テストする技術について検討する．手法の自動化・ツール化に取り組んだ後，提案手法を産業界由来の例題に適用し，実践的な成果を得ることを目指す．
（B）モンテカルロ法と制約ソルバーをより密に連携し，効率的に検証・テストする方法を検討する．
（C）（A）のツール実装の正しさを検証し，高信頼にすることを目指す．
（D）（B）による検証・テストツールの並列化を検討する．
|
| 次年度使用額が生じた理由 |
感染症の流行により，予定していた国内・海外の出張ができなかったため．また研究進捗の遅れにより，研究環境の整備が遅れたため．次年度に出張および研究環境整備を実施する予定である．
|
