|
無限小プログラミングに基づくハイブリッドシステム検証手法について研究を行った．ハイブリッドシステム検証手法としては未だ発展途上であるものの，その過程で非線形な不変条件の高速な生成手法という重要な知見が得られた．不変条件生成手法はプログラム検証において検証の成否を握る重要な要素技術であるが，既存の手法は非線形な不変条件を効率よく生成することが難しいことが多く，複雑なシステムの検証に困難が生じていた．本手法では次元解析の手法を用いることで，既存の非線形不変条件生成手法を高速化することが可能となった．研究期間終了後は本手法をさらに発展させ，より複雑なハイブリッドシステム検証手法につなげる予定である．
|
