Verification Techniques for Hybrid Systems based on Interval Constraint Programming and Deductive Reasoning

2014 Fiscal Year Final Research Report

• 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
• 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.

Free Research Field

ソフトウェア