2017 Fiscal Year Annual Research Report
Interval constraint programming technique for discrete-continuous hybrid systems
| Project/Area Number |
15K15968
|
|---|
| Research Institution | University of Fukui |
|---|
Principal Investigator |
石井 大輔 福井大学, 学術研究院工学系部門, 講師 (00454025)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | ハイブリッドシステム / 制約プログラミング / 区間制約 / 探索・論理・推論アルゴリズム |
|---|
| Outline of Annual Research Achievements |
ハイブリッドシステムの高信頼な解析を可能にすることを目標に、2017年度は下記の3項目を実施した。
(a) これまで、高信頼数値シミュレーションに基づきハイブリッドオートマトンを検査するツールとしてHySIAを開発してきたが、その整備を行った。時間的な性質に対する頑強性を区間値で計算する手法やウェブインターフェースを実装し、複数の解析例を示した。また、ツールの簡潔な実現方法として、ハイブリッドシステム記述用言語であるAcumenにより、HySIA同様の頑強性計算の機能を簡潔に実現する方法を検討した。Acumenツール上で統計的モデル検査を実施する例を示した。さらに、HySIAやAcumenをはじめとするツールの信頼性を高めるため、基本的な区間演算コードについて、ホーア論理とSMTソルバーを用いたプログラム検証を実施した。結果の区間値が、真解を包含し、かつtightなものであることを機械的に証明した。
(b) 大規模PCクラスタにおいて、最適化問題を並列探索に基づき求解するための枠組みとして、X10 GLBOライブラリを構築した。完全木に基づくベンチマーク問題を考案し、GLBOの評価実験を行った。求解中に暫定最適値を並列ワーカー間で効率よく共有する方法を実装し、504ワーカーによる求解において1.4倍程度の性能向上が得られることを確認した。
(c) MATLAB/Simulink で記述された小・中規模のモデルを収集し、テストケース生成や2モデル間の適合性検査のための静的解析の方法を検討した。モデルを制約充足問題に変換し、SMTソルバーと区間制約ソルバーで求解することにより、既存ツールでは静的解析が難しい場合も扱えることがわかった。非線形式を記述したモデルや中規模のモデルにおいても提案手法が有効であることを確かめた。
|
