2022 Fiscal Year Annual Research Report
Interval constraint programming techniques for large and complex hybrid systems
| Project/Area Number |
18K11240
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
石井 大輔 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | ハイブリッドシステム / 制約プログラミング / 区間解析 / 探索・論理・推論アルゴリズム |
|---|
| Outline of Annual Research Achievements |
連続・離散ハイブリッドシステムのための制約プログラミング技術を開発することを目標に，MATLAB/Simulinkで記述したモデルを検証・テストする手法について研究した．今年度はおもに3項目を実施した．
（1）Simulinkモデルとその安全性について検査する手法について研究した．提案手法は，モデルと安全性を述語論理式に変換し，それを既存のSMTソルバーで解くことにより検査を実施する．今年度は，産業界由来の例を扱うことを目指し，多様なモデルを効率よく検査するための複数の方法を設計・実装した．論理式に変換する際，モデルが含むサブシステムを抽象化したり，安全性と関連するモデル記述をスライシングしたりする方法を検討した．検査は，対象となるサブシステム階層数と信号の長さを調整しながら実施するが，これらの変数の値を反復深化させて検査する方法を検討した．また，38種類のブロック型や多様な連結構造を扱う方法を検討した．
（2）モンテカルロ法と（1）の手法を組み合わせたSimulinkモデルの網羅テスト手法について研究した．モンテカルロ法と手法（1）を順次用いる手法を設計・実装した．多様なモデルに対して効果的な両手法の切り替え条件を実験的に求めた．網羅テストに手法（1）を用いる際はテスト項目のリストについて反復的に検査していくが，効率的な処理方法を検討した．
（3）（1）と（2）の手法をMATLAB上に実装し，評価実験を行った．大規模複雑なSimulinkモデルの例として，人工的モデルと産業的モデルを約15例収集した．各モデルについて複数の安全性を証明・反証する実験と，網羅テストの実験を実施した．また，既存ツールとの比較実験を実施した．実験結果では，提案手法が正しく効率的に動作することと，実行時間やテスト網羅度について，既存ツールと比較して良好な性能が得られることがわかった．
|
