| 研究概要 |
本研究では、複雑化・高度化するシステムやソフトウェアを対象にして、その安全性や信頼性の向上を目指し,設計・開発の正当性・妥当性の形式的検証を可能とする計算論理的基盤技術の確立を目的とする.本研究の特徴は,形式的検証のための計算論理に基づく技術として,論理プログラムに対するプログラム変換による検証技術を中核に用いる点にある.本研究の提案者は,昨年度,層状論理プログラムに対する等価変換の枠組みにおいて,負リテラルに対する展開規則が従来研究の条件では不十分であることを示し,新しい適用条件を明らかにした.今年度はこの結果を基にして,それをシステムの性質を検証する推論のために用いる変換の枠組みの拡張を引き続き行い,以下のようなことを示した:
1.負リテラルに対する展開規則の拡張を提案した.従来研究では扱えないような場合でも適用可能な形式を与え,それを含んだ変換の枠組みを示した.
2.更に上記のプログラム変換システムに2つの変換規則,すなわち,斉時畳込み(simultaneous folding),負リテラルの畳込み(negative folding)を導入し,その正当性を証明した.
3.提案したプログラム変換に基づく証明システムが,従来研究でのプログラム変換によるプログラムの性質の証明方法と比較して,より単純で従って自動化しやすく,しかも直観的に分かりやすい方法で検証が実現できることを例により示した.
このようにプログラム変換技術を用いた検証方法の確立へ向けて基礎となる知見を得ることができた.
|
