Forma verification of hybrid systems based on the infinitesimal programming

2015 Fiscal Year Final Research Report

• Project/Area Number: 25730040
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Software
• Research Institution: Kyoto University
• Principal Investigator: Suenaga Kohei 京都大学, 情報学研究科, 准教授 (70633692)
• Project Period (FY): 2013-04-01 – 2016-03-31
• Keywords: ハイブリッドシステム / プログラム検証 / 不変条件 / 無限小プログラミング / 超準解析 / 次元解析 / 非線形不変条件 / システム検証

Outline of Final Research Achievements

We investigated a method for verifying hybrid systems based on the idea of the infinitesimal programming. Although the obtained result is yet to scale to practical hybrid systems, as a byproduct, we obtained an efficient nonlinear invariant synthesis algorithm. Invariant synthesis algorithms, which is an important technology in program verification, often cannot be applied to a complex system due to their complexity. Our method makes these algorithms fast using the idea of dimension analysis used in the are of physics. We plan to investigate this idea to an algorithm that can deal with more complex hybrid systems.

Free Research Field

プログラム検証