2018 Fiscal Year Research-status Report
大規模・複雑なハイブリッドシステムのための区間制約プログラミング技術
| Project/Area Number |
18K11240
|
|---|
| Research Institution | University of Fukui |
|---|
Principal Investigator |
石井 大輔 福井大学, 学術研究院工学系部門, 准教授 (00454025)
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Keywords | ハイブリッドシステム / 制約プログラミング / 区間解析 / 探索・論理・推論アルゴリズム |
|---|
| Outline of Annual Research Achievements |
連続・離散ハイブリッドシステム（以下HSとする）のための制約プログラミング技術を開発することを目標に、下記の4項目を実施した。
（a）HSモデリングツールであるMATLAB/Simulinkのためのテストケース自動生成手法を検討した。とくに大規模複雑なSimulinkモデルに対する有用なテストケースを得るための手法として、静的解析法とモンテカルロ法を連携した手法に取り組んだ。静的解析法として、区間制約ソルバーを用いる方法と、SMTソルバーを用いる方法を検討し、非線形制約に帰着されるモデルや中規模のモデルへ適用するための実装・実験を実施した。
（b）HSモデリング言語・ツールAcumenに関し、統計的モデル検査機能の追加と、形式的な意味論に基づく再実装を行なった。前者ではAcumenツールを用いた軽量な検証技術を提案し、Acumen上でモデリング、仕様記述、検証、結果の解析を実施する複数例を示した。後者では同ツール実装の高信頼化技術を開発した。
（c）制約プログラミング技術の高信頼実装のためのプログラム検証技術に取り組んだ。高信頼数値計算のための区間演算コード（四則演算や累乗）と、制約式に基づくモデル検査アルゴリズムを定理証明支援系やSMTソルバーを用いて検証した。最新の証明器を利用した高信頼実装の例を蓄積した。
（d）制約付き最適化問題の探索に基づくソルバーのための大規模並列化技術を開発した。PCクラスタ上で負荷分散と暫定最適解の分散とを両立させるための技術を検討した。木構造に基づくベンチマーク問題について性能評価実験を行ない、784コア使用時に429-824倍の速度向上を達成した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画に従い、「研究実績の概要」に記載の4項目について研究を進めた。（a）大規模複雑なMATLAB/Simulinkモデルの解析が可能な制約プログラミング技術、（b）統計的にハイブリッドシステムの振る舞いを解析する手法、（c）区間演算やモデル検索器のためのプログラム検証、（d）探索に基づく最適化問題の並列求解処理のそれぞれに関して成果を得ることができたため、おおむね順調に進展している。
|
| Strategy for Future Research Activity |
計画に従い、ハイブリッドシステムのための制約プログラミング技術開発を進める。
（a-b）より大規模なSimulinkモデルに対して適用するための開発・実験を行う。そのためには基本的な線形制約の求解を高速に実施することが重要となる。線形制約ソルバーを別途開発し、提案手法へ組み込むことを検討する。
（c）区間演算と探索を組み合わせたプログラムや、多様かつ実用的なモデル検査アルゴリズムの検証を実施する。
（d）数値制約付き最適化問題を区間解析に基づき求解するソルバーの並列化を実施する。
|
| Causes of Carryover |
（理由）当初計画していた（海外での）国際会議発表を行なわなかったため。
（使用計画）研究成果の国際会議発表を行う。また、海外での車載システム研究開発に関して調査を行う。
|
