| 研究課題/領域番号 |
18K11240
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
石井 大輔 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2022-03-31
|
| キーワード | ハイブリッドシステム / 制約プログラミング / 区間解析 / 探索・論理・推論アルゴリズム |
|---|
| 研究実績の概要 |
連続・離散ハイブリッドシステム（以下HSとする）のための制約プログラミング技術を開発することを目標に、下記の3項目を実施した。
（1）HSモデリングツールであるMATLAB/Simulinkのための検証およびテスト手法を検討した。とくにSMTソルバーを活用して安全性検査およびテストケース生成を実施する手法と、大規模なSimulinkモデルを扱うため、数値シミュレーションで得たパス制約を用いてテストケース生成を効率化する手法について研究した。検討した結果をツール化し、中規模モデルについてフルカバレッジテストが実施できることを実験により確かめた。また、前記手法において、多数の同形の制約を連立して解く必要があるため、同形の制約を効率よく扱うための手法について研究した。
（2）制約プログラミング処理系の高信頼実装のためのプログラム検証技術に取り組んだ。昨年度から継続し、高信頼数値計算のための区間演算コード（四則演算や累乗）と、制約充足に基づくモデル検査アルゴリズムを、定理証明支援系やSMTソルバーを用いて検証した。前者については演算結果がtightであることの検証に取り組み、後者についてはPDR法の形式化とアルゴリズムの健全性証明の形式化に取り組んだ。それぞれの検証結果を論文にまとめ、論文誌JCAMと国際会議TASEにおいて受理された。
（3）数値制約付き最適化問題の探索に基づくソルバーのための大規模並列化技術を開発した。最小解の上界を区間で近似する方法、暫定的な近似解を並列ワーカー間で共有、探索空間の枝刈りに役立てる方法などについて研究を実施した。当該技術を実装し、PCクラスタ上での実験により効果を確かめた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初計画した研究項目（A）～（D）のうち3項目について、「研究実績の概要」に記載したように研究を進めた。
（1/研究項目A）大規模複雑なMATLAB/Simulinkモデルの解析が可能な制約プログラミング技術、
（2/研究項目C）区間演算やモデル検索器のためのプログラム検証、
（3/研究項目D）探索に基づく最適化問題の並列求解処理のそれぞれに関して成果を得ることができたため、おおむね順調に進展している。
研究項目（B）の統計的なハイブリッドシステムの解析手法に関しては、（A）の成果をモンテカルロ法に基づく手法と連携したものを検討しているが、本年度は（A）単体の研究を進めた。
|
| 今後の研究の推進方策 |
計画に従い、ハイブリッドシステムのための制約プログラミング技術開発を進める。
（A）大規模なSimulinkモデルを部分システムに分割して検証・テストする技術について検討する。またハイブリッドシステムを制約式に変換する方法を複数検討し、効率的な方法を実験的に明らかにすることを目指す。
（B）（A）による解析結果とモンテカルロ法を連携してより大規模複雑なSimulinkモデルを扱う方法を検討する。
（C）複数の区間演算方式を扱えるようモジュール化した、検証済み実装の実現を目指す。制約充足に基づく実用的なモデル検査器の完全性証明を形式化し、実用可能な検証済み実装の実現を目指す。
（D）（B）による検証・テストツールの並列化を検討する。
|
| 次年度使用額が生じた理由 |
（理由）当初計画していた物品購入や国際会議発表を行なわなかったため。
（使用計画）物品購入と研究成果の国際会議発表を行う。
|
