2013 Fiscal Year Research-status Report
無限小プログラミングによるハイブリッドシステムの形式検証手法
| Project/Area Number |
25730040
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | ハイブリッドシステム / プログラム検証 / プログラム理論 / プログラム意味論 |
|---|
| Research Abstract |
本研究課題においては，ソフトウェアのための形式検証（数理的手法に基づいてソフトウェアの性質を厳密に検証する手法）をハイブリッドシステム（離散的動作と連続的動作を併せ持つシステム）の検証に適用することを目指している．その際に困難になるのは，ソフトウェア検証手法が予定していない連続的動作の存在である．この解決のために，研究代表者らによって提案された無限小プログラミング言語（無限小を表す定数を備えた，厳密に意味論が定義されたプログラミング言語）を用いて，連続的動作を無限回の無限小動作で置き換え，その上でソフトウェア検証手法を適用する．
前年度から本年度にかけての実験において，現状のソフトウェア形式検証手法ではハイブリッドシステム検証に不十分な点があることが明らかになった．具体的には，現状のソフトウェア形式検証手法は検証すべき性質や，検証の過程で現れるシステムの性質を表す式が，線形不等式の論理結合で表されているものをターゲットにしていることが多く，ハイブリッドシステムに頻出する非線形な性質を扱うのが必ずしも容易ではないという点である．この問題を解決するため，今年度はプログラム検証分野のみならず制御理論や代数幾何学等，多分野において非線形な性質を扱っている分野の成果を参照しつつ，非線形な性質を扱うことのできる検証手法のアイデアを探索した．その結果，いくつかの有望そうなアイデアが見つかったため，これらのアイデアについて研究を進めている段階である．
また，無限小プログラミングとはやや手法を異にするが，ハイブリッドシステムの入力生成，すなわち，システムを指定した通りに動作させる入力信号列を計算する手法を提案し，論文として出版した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
今後無限小プログラミングに基づくハイブリッドシステム検証を進める上で非線形性を扱えるようにすることは不可欠である．今年度行った研究で，この非線形性に対応するための重要なアイデアがいくつか生まれており，今後の研究の土台となるとみられる．
|
| Strategy for Future Research Activity |
今年度得られたアイデアをさらに研究し，次年度は引き続き検証アルゴリズムの設計と実装を行う．ただし，現時点で得られているアイデアは計算量の観点から大きなシステムにそのままスケールするかどうかは現時点で不明である．今後は検証能力と計算量とのトレードオフの解決を念頭に置きつつ研究をすすめる方針である．
|
| Expenditure Plans for the Next FY Research Funding |
本年度の進捗が主に理論面に関する事項であったため，旅費・人件費が計画額よりも少なくなったものである．
次年度以降，本年度予定していた出張ならびに研究補助のための雇用を行う予定である．
|
