2015 Fiscal Year Annual Research Report
無限小プログラミングによるハイブリッドシステムの形式検証手法
| Project/Area Number |
25730040
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | ハイブリッドシステム / 超準解析 / プログラム検証 / 不変条件 / 次元解析 |
|---|
| Outline of Annual Research Achievements |
ループ不変条件生成手法の研究を行った．ループ不変条件生成手法は，プログラム検証において一般的に用いられる重要な要素技術であり，プログラム中で常に成り立つ条件で検証すべき性質を証明できる程度に強力な条件を求める手法である．これまでにプログラムを対象としたループ不変条件生成手法はいくつか提案されてはいるものの，その多くはプログラム変数の線形結合で表現される条件のみが扱えるものであった．ハイブリッドシステムを扱うにあたっては非線形性の関わる条件を扱う必要があるために，これらの手法をそのまま適用することは難しいことが分かった．非線形性を含む不変条件を生成できる手法としては [Cachera et al. 2014, Muller-Olm et al. 2004, Rodriguez-Carbonell et al. 2007, Sankaranarayanan et al. 2004] があるが，これらの手法は計算コストが高く，複雑なシステムにスケールさせるのが難しい．そのため，本研究ではこれらの非線形条件が扱える不変条件生成手法を高速化させるための研究を行った．
本研究では，プログラムを事前に解析することでテンプレートのサイズを削減する手法を研究した．ハイブリッドシステムはメカ・エレキと呼ばれる物理現象が関わる系を含むシステムである．そのため，生成すべき不変条件は物理的に意味のある量が関わる条件になるべきであると期待される．この直観に基づき本研究では，プログラムに対して次元解析を行う既存手法 [Kennedy 1994] を適用した上で，物理次元の合ったテンプレートのみを生成するように不変条件生成手法を改良した．これにより，物理的に意味のない巨大なテンプレートを生成することを防ぐことができる．従来手法に比して現実的なプログラムにおいて最大10倍程度の高速化が達成された．この成果について2件の特許出願を行っている．
|
