|
本研究は，リアクティブ・システム等のソフトウェアの正当性を形式的に検証するための方法論の構築を目的とする．そのために，計算論理に基づく形式手法である論理プログラムに対するプログラム推論を用いるアプローチを採用し，次のような3つの主な研究成果を得た．(1) 余論理プログラムに対するプログラム推論とそれを用いた仕様の検証法を示した．(2) その結果を拡張し，ソフトウェアの正当性検証問題であるCTL時間論理式に対するモデル検査を実現できることを示した． (3) 検証に必要となるプログラムの仕様を効率的に発見するための基礎となるパターン・マイニング方法を示した．
|
