2017 Fiscal Year Annual Research Report
Verifying Software Systems using Reasoning about Programs Handling Infinite Structures
| Project/Area Number |
15K00305
|
|---|
| Research Institution | Nagoya Institute of Technology |
|---|
Principal Investigator |
世木 博久 名古屋工業大学, 工学(系)研究科(研究院), 教授 (90242908)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | 探索・論理・推論アルゴリズム / 計算論理 / プログラム推論 |
|---|
| Outline of Annual Research Achievements |
本研究では，リアクティブ・システムなどの状態が無限に継続する対象を扱うソフトウェアの正当性を検証する検証システム構築のための方法論を確立することを目的としている．そのために，計算論理に基づく論理プログラムに対するプログラム推論技術を中核に用いる点が特徴である．
本研究で対象とする論理プログラムは，リアクティブ・システムの記述に必要な無限構造を自然に扱える余論理(co-logic)プログラムを基礎としている． その余論理プログラムとホーンμ-計算 (Horn μ-calculus)との関連性に着目し，その性質とプログラム推論方法についての検討を行った．そのなかで，ホーンμ-計算が余論理プログラムをその一クラスとして扱えるより一般的な枠組みであることを示した．また，論理プログラムにおける主要な意味論である有礎モデルと解集合を取り上げ，ホーンμ-プログラムとの関係を調べた．
また，プログラム検証に必要な仕様をユーザがあらかじめ正確に与えることは難しい問題である. そのために, 実行ログから自動的に導出する仕様発見のアプローチを採用した. プログラム実行のログを格納した系列データから再現(recurrent)ルールというパターンを発見する仕様発見アルゴリズムについて，効率の良いアルゴリズムの検討と実装を行った．また，仕様表現に必要とされる時間等の量的制約を表現する区間パターン発見アルゴリズムの設計と効率的な実現も行った．
本研究の結果から，モデル検査などのシステム検証問題に対して余論理プログラムやホーンμ-計算を用いた計算論理に基づく推論方法の有効性を示す知見を得た．このことは，仕様発見機能を備えたプログラム推論に基づくシステムの検証方法の実現に貢献する意義がある．
|
Research Products
(5 results)
