2015 Fiscal Year Annual Research Report
無限項を扱うプログラム変換を用いたソフトウェア検証方法の研究
| Project/Area Number |
24500171
|
|---|
| Research Institution | Nagoya Institute of Technology |
|---|
Principal Investigator |
世木 博久 名古屋工業大学, 工学(系)研究科(研究院), 教授 (90242908)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Keywords | 探索・論理・推論アルゴリズム / 計算論理 / プログラム推論 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は，リアクティブ・システムなどのソフトウェアの正当性を検証する検証システムのための方法論を構築することである．そのために，計算論理に基づく形式的手法の一つである論理プログラムに対するプログラム推論技術を用いるアプローチを採用した．
本研究では，リアクティブ・システムの記述に不可欠な無限項を容易に扱える余論理(co-logic)プログラムに注目した．まず，余論理プログラムに対するプログラム推論とそれを用いた仕様の検証方法を示した．次に， ソフトウェアの正当性検証の問題としてCTL時間論理式に対するモデル検査問題を取り上げて，従来の最良なオートマタ理論による方法を，余論理プログラムを拡張した枠組みを用いて実現できることを示した．また，より一般的で記述能力の高い枠組みとして，ホーンμ-計算に注目した．そして，ホーンμ-プログラムが余論理プログラムの真の拡張であることを示し，またホーンμ-プログラムのための実際的な推論方法を与えた．更に，検証するプログラムの性質（仕様）をプログラムの実行からマイニングにより発見する方法についても検討した．
研究計画の最終年度では，これまでに検討した仕様マイニングの基礎となるパターンマイニング・アルゴリズムについて詳細検討をすすめ，そのアルゴリズムを実装して動特性の解析を行った．
また，検証システムの実現については，CTL時制論理に対するモデル検査方法を，余論理プログラミング技術を利用したシステムの実現方法を示し，それを余論理プログラムの処理系を利用し実装している．
以上から，モデル検査などのシステム検証問題に対して余論理プログラムを用いた推論方法によるアプローチが有効で効率的な実装につながるという知見を得た．またこれは，プログラム推論に基づくシステム検証のための方法論の基礎となる点で意義がある．
|
