|
本研究は，リアクティブ・システムなど無限に継続する状態を扱うソフトウェアの正当性検証に向けた方法論の確立を目的とする．そのために，計算論理に基づくプログラム推論技術を中核に用いる点に特徴がある．次のような3つの研究成果を得た．(1) 推論に用いる余論理プログラム(co-logic programs) とホーンμ-計算 (Horn μ-calculus)に関する諸性質やその応用を示した．(2) 検証に必要な仕様を実行ログから導出する仕様発見アルゴリズムを提案した. (3) 仕様表現に必要とされる時間等の量的制約も含むパターン発見アルゴリズムの設計と効率的な実装を行った．
|
