Verification Techniques for Hybrid Systems based on Interval Constraint Programming and Deductive Reasoning
| Project/Area Number |
25880008
|
|---|
| Research Category |
Grant-in-Aid for Research Activity Start-up
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
ISHII Daisuke 東京工業大学, 情報理工学(系)研究科, 助教 (00454025)
|
|---|
| Project Period (FY) |
2013-08-30 – 2015-03-31
|
| Project Status |
Completed (Fiscal Year 2014)
|
| Budget Amount *help |
¥2,730,000 (Direct Cost: ¥2,100,000、Indirect Cost: ¥630,000)
Fiscal Year 2014: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2013: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | ハイブリッドシステム / 制約プログラミング / 区間解析 / 探索・論理・推論アルゴリズム / 並列分散処理 / 国際研究者交流 / 並列計算 / 演繹的推論 / 国際研究者交流: フランス、スウェーデン |
|---|
| Outline of Final Research Achievements |
We have developed techniques for verifying various properties (e.g., safety and stability) about hybrid systems that involve continuous and discrete behaviors, using interval constraint programming and deductive reasoning. Development of this research is based on the notion of constraints that integrates reliable numerical computation and symbolic computation (e.g., formula manipulation and temporal logic verification). We have built (i) a parallel interval constraint solver that handles efficiently nonlinear arithmetic constraints, and (ii) a verifier for hybrid systems based on the constraint solver. In the experiments, we have shown that several models, which are difficult to handle with existing tools, can be verified with our tools.
|
Report
(3 results)
Research Products
(9 results)
