Forma verification of hybrid systems based on the infinitesimal programming
| 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
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2015: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2014: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
Fiscal Year 2013: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| 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.
|
Report
(4 results)
Research Products
(16 results)
-
-
-
-
-
-
-
-
[Presentation] 京都大学 Teen Racketeer 養成コース2015
Author(s)
五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 大元 武, 宮本 洋平, 末永 幸平
Organizer
第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015）
Place of Presentation
愛媛県松山市道後プリンスホテル
Year and Date
2015-03-04 – 2015-03-06
Related Report
-
-
-
-
-
-
-
-
