2018 Fiscal Year Research-status Report
無限構造を扱うシステムの検証に向けた仕様発見系を持つプログラム推論技術の研究
| Project/Area Number |
18K11432
|
|---|
| Research Institution | Nagoya Institute of Technology |
|---|
Principal Investigator |
世木 博久 名古屋工業大学, 工学(系)研究科(研究院), 教授 (90242908)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | プログラム推論 / 仕様マイニング / パターン発見 |
|---|
| Outline of Annual Research Achievements |
本研究では，リアクティブ・システムなどのソフトウェアを対象に，その正当性を検証する検証システムの構築に向けた方法の確立を目的としている．検証システムにおける推論系として，先行研究で行った余論理(co-logic)プログラムと呼ばれる論理プログラムに対するプログラム推論等の計算論理に基づく形式的手法を基礎として利用する．研究計画1年目では，そのプログラム検証系の入力である対象システムの仕様式を実行ログ集合から自動的に導出する仕様発見系について検討を行った．特に，プログラム実行のログを格納した系列データから再現(recurrent)ルールというパターンを発見する仕様発見アルゴリズムについて，より効率的なアルゴリズムの設計を進めた．また，そのアルゴリズムに内在する並列性を活かした並列実装方式を試作し，実験結果を蓄積した．
また，仕様検証の結果，ソフトウェアシステムが仕様を満たしていない場合，プログラムのどこにバグがあるかを特定する必要が生ずる．本研究では，形式概念分析(FCA)とパターンマイニングの一方法である相関ルールを用いて，バグの位置特定を行う方法を想定している．その設計を進めるとともに, 区間パターン等の制約を持つ相関ルール発見アルゴリズムの効率的な実現方法の検討を行った．また，FCAに基づく相関ルールの応用として，テキスト文書の分類への適用可能性についても調査を行った．
これまでの研究結果から，ソフトウェア・システムなどの検証問題に対し，論理プログラムの推論方法を用いて仕様式を検証し，その仕様式はパターン発見技術により導出するという枠組みの基礎となる知見が得られた．これは，プログラム推論とパターン発見技術に基づくシステムの検証方法の開発に貢献する意義がある．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究では，システム検証のための計算論理に基づく推論系に，検証対象の仕様式を与える仕様発見系を融合した検証システムの構築を目的とする．このために，先行研究で行ったプログラム検証のためのプログラム推論系に基づき，仕様式を発見する仕様マイニングのためのパターン発見技術の蓄積，そして仕様式が満たされていない場合にプログラム中のバグの箇所を特定する方法について，方式設計, 試作・実験,その有効性・妥当性の実証という研究サイクルを遂行するための課題を設定している．研究計画１年目は，特に以下のような研究課題について研究を行った．
プログラム検証の対象となる仕様をログから発見する仕様マイニングについては，ログ系列データから再現ルール発見アルゴリズムについて複数のアプローチを検討し，その実装を行った．また，その並列化等の効率的な実現についての見通しを得た．この点ではほぼ予定通り順調に進行している．
また，仕様検証の結果，対象システムが仕様を満たしていない場合に，プログラム中のバグの位置を特定する方法については，形式概念分析(FCA)と相関ルール・マイニングを用いて，バグの位置特定を行う手法について検討を進めた．その設計のために，区間パターン等の制約を持つ相関ルール発見アルゴリズムの実装を行った．また，他の応用分野についても調査を行った．この結果，バグの位置特定法に向けて，効率的な実現可能性についての見通しを得て，概ね予定通りに進行している．
計算論理に基づく推論系に仕様発見系を融合した検証システムのアプローチの有効性を確認するための実験については，再現ルールから導出される時制論理式を対象にして，それを検証するためのシステム実現に向けて，系列パターンマイニング技術を用いた方法の有効性を確認した． 以上から，研究計画に従ってほぼ予定通り順調に進行している．
|
| Strategy for Future Research Activity |
これまでに検討してきた設計方式と実験の結果に基づいて，システム検証のため推論系と検証対象の仕様式を得る仕様発見系を融合した検証システムの構築に向けて，提案方式の改良と拡張を引き続き行う．具体的には，以下のようなタスクについて研究を進める．
プログラム検証の対象となる仕様をログから発見する仕様マイニングについては，ログ系列データから再現ルール発見アルゴリズムについて複数のアプローチの評価実験結果に基づき，引き続き検討をすすめる．これにより計算コストの高い再現ルールマイニングのための効率的なアルゴリズムと実装技術の確立を目指す．
また，ソフトウェアシステムが仕様を満たさないことが判明した場合に，プログラム中のバグの位置特定法については，形式概念分析(FCA)と相関ルール・マイニングを用いた手法に関して検討を継続する．プログラムの実行時の経路を抽出するツールの利用やその結果から形式概念における文脈に変換する処理を早期に実現することを目指す．これまでの調査結果をもとに，バグの位置特定法の効率的な実現を図る．
システム検証のため推論系と検証対象の仕様式を得る仕様発見系を融合した検証システムの実現については，時制論理式に対するモデル検査のための余論理プログラムの証明手続きを利用したシステムについて，ベンチマークとして使われている例題を中心にして動作確認し本方式の有効性を評価する．特に，モデル検査等の従来研究での検証方式と比較検討して，本方式の有効性を評価しその妥当性を検討する．
以上のプロセスを通じて，プログラム推論系と検証対象の仕様発見系を融合したシステム検証の新しい枠組みの確立を目指す．
|
