| 研究課題/領域番号 |
18K11240
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
石井 大輔 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2022-03-31
|
| キーワード | ハイブリッドシステム / 制約プログラミング / 区間解析 / 探索・論理・推論アルゴリズム |
|---|
| 研究実績の概要 |
連続・離散ハイブリッドシステムのための制約プログラミング技術を開発することを目標に、モデリングツールであるMATLAB/Simulinkのための検証およびテスト手法を検討した。今年度はおもに3項目を実施した。
（1）大規模複雑なSimulinkモデルを部品化して検査する手法について研究した。探索に基づくモデル検査を検討してきたが、大規模複雑なモデルを直接扱うのは原理的に難しい。そこで半自動的にモデルを部品化し、部品ごとに検査する手法を検討した。また部品の検査結果から全体に関する結果を推論する手法も検討した。提案手法を既存手法で扱えなかった複数の例題に適用したところ、検査が可能となることが確認できた。現在、手法の自動化を検討している。また、モデル中の部品を動的に切り出しながら検査することにより、効率よく安全性検証をおこなう手法を検討した。本手法が有効な例題を複数収集し、実験的に効果を確認した。
（2）数値誤差を考慮しながらSimulinkモデルを検査する手法について研究した。（1）の検査では理想化した実数と整数に基づくモデルを対象としているが、浮動小数点数や固定小数点数に基づく現実的なモデルと異なる振る舞いをする場合が生じてしまう。そこで、区間解析に基づき状態を抽象化しながら検査する手法を検討した。その結果、現実的なモデルに対する検査結果を（既存手法を用いた場合に較べ）効率よく得られることが実験的に確認できた。現在手法の定式化と評価実験を進めている。
（3）（1）の部品化手法の推論過程を形式化し、SMTソルバー等を用いて自動検証することを可能にした。また（2）の区間解析手法について、昨年度の成果に基づき正しさの検証に取り組んだ。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
今年度は、当初計画していた「研究実績の概要」のうちの2項目
（A）大規模複雑なMATLAB/Simulinkモデルの解析が可能な制約プログラミング技術と、
（C）区間演算やモデル検索器のためのプログラム検証
に注力して研究を進めたため、達成目標全体に対する進捗がやや遅れている。
各項目について部分的な成果は得られているものの、実際のSimulinkモデル群に適用可能かつ自動的に実行可能な手法の実現を目指しているため検討事項が多く、まとまった成果発表に至っていない。その他の項目（B）と（D）については（A）と（C）の成果を得た後に取り組む予定である。
|
| 今後の研究の推進方策 |
計画の達成を目指し、ハイブリッドシステムのための制約プログラミング技術開発を進める。
（A）大規模複雑なSimulinkモデルを部品に分割して検証・テストする技術について検討する。手法の自動化に取り組んだ後、提案手法を産業界由来の例題に適用し、実践的な成果を得ることを目指す。ハイブリッドシステムをシミュレーションする際に発生する数値誤差を考慮しながら制約式に変換する方法を検討し、実用的な検証・テスト手法の実現を目指す。またこれらの手法のツール化に取り組む。
（B）（A）による解析結果と、研究連携者が取り組んでいるモンテカルロ法に基づく検証・テスト技術を連携してより大規模複雑なSimulinkモデルを扱う方法を検討する。
（C）複数の区間解析ツールに応用できるように、区間解析の形式検証の結果を一般化・整備することを目指す。区間累乗演算や他の初等関数の検証に取り組む。（A）のツールの実装を検証済みで高信頼にすることを目指す。
（D）（B）による検証・テストツールの並列化を検討する。
|
| 次年度使用額が生じた理由 |
（理由）当初計画していた物品購入や国際会議発表を行なわなかったため。
（使用計画）物品購入と研究成果の国際会議発表を行う。
|
