2009 Fiscal Year Annual Research Report
セキュアシステム構築のための計算論理的基盤技術の研究
| Project/Area Number |
21500136
|
|---|
| Research Institution | Nagoya Institute of Technology |
|---|
Principal Investigator |
世木 博久 Nagoya Institute of Technology, 大学院・工学研究科, 教授 (90242908)
|
|---|
| Keywords | プログラム変換 / システム検証 / 推論アルゴリズム / 計算論理 |
|---|
| Research Abstract |
本研究では、複雑化・高度化するシステムやソフトウェアを対象にして、その安全性や信頼性の向上を目指し,設計・開発の正当性・妥当性の形式的検証を可能とする計算論理的基盤技術の確立を目的とする.本研究の特徴は,形式的検証のための計算論理に基づく技術として,論理プログラムに対するプログラム変換による検証技術を中核に用いる点にある.本研究の提案者は,先行研究で局所層状論理プログラムに対するプログラムの等価変換の枠組みを提案している.今年度は,この枠組みを基にして,それをシステムの性質を検証する推論のために変換の枠組みの拡張を行い,その性質について以下のようなことを示した:
1.負リテラルに対する展開規則の新しい適用条件を提案した.従来研究で提示されている条件では不十分な場合があることを示し,その問題点を解決する変換の枠組みを与えた.
2.従来よりも一般的なゴール置換規則を与え,その正当性を証明した.
3.提案したプログラム変換に基づく証明システムが,Jaffarらによって提案されている余帰納法(双対帰納法)による証明システムと同等以上の推論能力を持つことを証明した.この目的のために,ゴール置換規則を拡張して"健全な"ゴール置換規則を導入した.これにより,検証のための特別な帰納法の推論スキーマを用いることなく,畳み込み及びゴールの置換えなどのプログラム変換規則の適用によって同等の帰納的推論が実現できることが分かった.
|
