| Project/Area Number |
18K11240
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology (2019-2022)
University of Fukui (2018) |
|---|
Principal Investigator |
Ishii Daisuke 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2021: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2020: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2019: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2018: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Keywords | ハイブリッドシステム / 制約プログラミング / 区間解析 / 探索・論理・推論アルゴリズム |
|---|
| Outline of Final Research Achievements |
To develop constraint programming techniques for discrete/continuous hybrid systems (HS), we have conducted a research on methods and tools for reliable and practical analyses on HS that models large-scale and complex embedded systems. The proposed methods include a safety model checker and an optimizer of objective functions based on constraint programming techniques. The proposed methods encode HS described with Simulink and Acumen into constraints involving variables in the domains of reals, floating-point numbers, intervals, etc., and then analyze them using solvers. We have confirmed the performance and effectiveness of the proposed methods by the experiment with industrial model examples. We have also performed a formal verification of the correctness of the basic methods and implementations.
|
| Academic Significance and Societal Importance of the Research Achievements |
学術的意義として，一般的には扱うのが難しい大規模複雑なハイブリッドシステムを解析する手法の開発に取り組み，その効果を示す実験結果を得たことが挙げられる．有用な実例を検査するため，制約への符号化法，部品や繰り返しを考慮した検査法，モンテカルロ法との連携，大規模並列化，提案手法の実装技術等，複数の面について研究した．また，手法・実装自体の検証に取り組み，形式手法の研究過程の機械化・高信頼化を進めた意義がある．
社会的意義として，提案手法を実世界で稼働するシステムに対して適用し，そのモデルの安全性検査等に役立てられることが挙げられる．
|
