2011 Fiscal Year Annual Research Report
セキュアシステム構築のための計算論理的基盤技術の研究
| Project/Area Number |
21500136
|
|---|
| Research Institution | Nagoya Institute of Technology |
|---|
Principal Investigator |
世木 博久 名古屋工業大学, 大学院・工学研究科, 教授 (90242908)
|
|---|
| Keywords | プログラム変換 / システム検証 / 推論アルゴリズム / 計算論理 |
|---|
| Research Abstract |
本研究では、複雑化・高度化するシステムやソフトウェアを対象にして、その安全性や信頼性の向上を目指し,設計・開発の正当性・妥当性の形式的検証を可能とする計算論理的基盤技術の確立を目的とする.本研究の特徴は,形式的検証のための計算論理に基づく技術として,論理プログラムに対するプログラム変換による検証技術を中核に用いる点にある.
昨年度から引き続いて,システムの様々な性質を検証するために必要な推論方法の見直しを進めていたが,従来のプログラム変換の枠組みを拡張して,余論理プログラム(co-logic programs)を対象とした新しいプログラム変換規則とそれを用いた検証方式の定式化を行った.その結果,以下の研究成果を得ることができた:
1.従来の論理プログラムに対するプログラム変換規則では,余論理プログラムの場合には不十分であることを示し,新しい適用条件を明らかにした.
2.通常のプログラム変換規則である定義の導入,展開,畳込みの3規則に加えて,余論理プログラム用に設計したゴール置換規則を導入し,その正当性を証明した.
3.提案したプログラム変換に基づく証明システムが,従来研究でのプログラム変換によるプログラムの性質の証明方法と比較して,より単純で従って自動化しやすく,しかも直観的に分かりやすい方法で検証が実現できることを例により示した.
余論理プログラムでは無限項を扱うことができるので,リアクティブ・システムを対象としてその性質を検証することが可能となった.このように,プログラム変換技術を用いたリアクティブ・システムの検証方法の確立へ向けて基礎となる知見を得ることができた点で意義がある.
|
