連続変化と離散変化の振る舞いをするハイブリッドシステムに対する,安全性や安定性といった性質の検証を,区間制約プログラミングと演繹的推論を用いて実施するための技術を開発した.本研究は,制約概念を軸に,高信頼な数値計算と,数式処理や時相論理式検証などの記号計算とを統合した点を特色とする.非線形算術制約を高速に求解する並列区間制約ソルバーを構築するとともに,本ソルバーを利用したハイブリッドシステムの検証器を構築,既存ツールでは検証が難しかった複数の事例について,提案ツールにより検証可能であることを示した.
|